diff --git a/proof/crefine/AARCH64/Finalise_C.thy b/proof/crefine/AARCH64/Finalise_C.thy
index a9eb23f0d5..4ad5f2df7b 100644
--- a/proof/crefine/AARCH64/Finalise_C.thy
+++ b/proof/crefine/AARCH64/Finalise_C.thy
@@ -316,7 +316,6 @@ lemma cancel_all_ccorres_helper:
         Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
          (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
        OD)"
-find_theorems ccorres_underlying name: cross
   unfolding whileAnno_def
 proof (induct ts)
   case Nil
diff --git a/proof/crefine/ARM/Finalise_C.thy b/proof/crefine/ARM/Finalise_C.thy
index 069066b17e..b6f1eccdb7 100644
--- a/proof/crefine/ARM/Finalise_C.thy
+++ b/proof/crefine/ARM/Finalise_C.thy
@@ -314,7 +314,6 @@ lemma cancel_all_ccorres_helper:
         Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
          (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
        OD)"
-find_theorems ccorres_underlying name: cross
   unfolding whileAnno_def
 proof (induct ts)
   case Nil
diff --git a/proof/crefine/ARM_HYP/Finalise_C.thy b/proof/crefine/ARM_HYP/Finalise_C.thy
index 4738ffcb14..7754226d0c 100644
--- a/proof/crefine/ARM_HYP/Finalise_C.thy
+++ b/proof/crefine/ARM_HYP/Finalise_C.thy
@@ -314,7 +314,6 @@ lemma cancel_all_ccorres_helper:
         Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
          (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
        OD)"
-find_theorems ccorres_underlying name: cross
   unfolding whileAnno_def
 proof (induct ts)
   case Nil
diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy
index 3afbf935e8..8008854dd0 100644
--- a/proof/crefine/RISCV64/Finalise_C.thy
+++ b/proof/crefine/RISCV64/Finalise_C.thy
@@ -333,7 +333,6 @@ lemma cancel_all_ccorres_helper:
         Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
          (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
        OD)"
-find_theorems ccorres_underlying name: cross
   unfolding whileAnno_def
 proof (induct ts)
   case Nil
diff --git a/proof/crefine/X64/Finalise_C.thy b/proof/crefine/X64/Finalise_C.thy
index d9d04ae60d..8448f58e94 100644
--- a/proof/crefine/X64/Finalise_C.thy
+++ b/proof/crefine/X64/Finalise_C.thy
@@ -315,7 +315,6 @@ lemma cancel_all_ccorres_helper:
         Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
          (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
        OD)"
-find_theorems ccorres_underlying name: cross
   unfolding whileAnno_def
 proof (induct ts)
   case Nil