# HG changeset patch
# User haftmann
# Date 1747578781 0
# Node ID 2bb4a8d0111d64d045e4b60c4e01634fb9cc8bbc
# Parent  9c4daf15261cd40b419cd78a664c0def60f4a95e
dropped unused ML bindings

diff -r 9c4daf15261c -r 2bb4a8d0111d NEWS
--- a/NEWS	Fri May 16 20:44:51 2025 +0200
+++ b/NEWS	Sun May 18 14:33:01 2025 +0000
@@ -75,6 +75,15 @@
 
 *** HOL ***
 
+* ML bindings for theorms Ball_def, Bex_def, CollectD, CollectE, CollectI,
+Collect_conj_eq, Collect_mem_eq, IntD1, IntD2, IntE, IntI, Int_Collect, UNIV_I,
+UNIV_witness, UnE, UnI1, UnI2, ballE, ballI, bexCI, bexE, bexI, bex_triv, bspec,
+contra_subsetD, equalityCE, equalityD1, equalityD2, equalityE, equalityI,
+imageE, imageI, image_Un, image_insert, insert_commute, insert_iff,
+mem_Collect_eq, rangeE, rangeI, range_eqI, subsetCE, subsetD, subsetI,
+subset_refl, subset_trans, vimageD, vimageE, vimageI, vimageI2, vimage_Collect,
+vimage_Int, vimage_Un. INCOMPATIBILITY, use thm(s) antiquotation instead.
+
 * Normalization by evaluation (method "normalization", command value) could
 yield false positives due to incomplete handling of polymorphism in certain
 situations; this is now corrected.
diff -r 9c4daf15261c -r 2bb4a8d0111d src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Sun May 18 14:33:01 2025 +0000
@@ -850,7 +850,7 @@
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
          (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
-           (insert_commute RS ssubst) 1),
+           (@{thm insert_commute} RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ctxt 1,
        REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Message.thy	Sun May 18 14:33:01 2025 +0000
@@ -830,7 +830,7 @@
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
          (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
-           (insert_commute RS ssubst) 1),
+           (@{thm insert_commute} RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ctxt 1,
        REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Auth/OtwayReesBella.thy
--- a/src/HOL/Auth/OtwayReesBella.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy	Sun May 18 14:33:01 2025 +0000
@@ -239,8 +239,8 @@
 
 val analz_image_freshK_ss =
   simpset_of
-   (\<^context> delsimps [image_insert, image_Un]
-      delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
+   (\<^context> delsimps @{thms image_insert image_Un}
+      delsimps @{thms imp_disjL}    (*reduces blow-up*)
       addsimps @{thms analz_image_freshK_simps})
 
 end
@@ -249,7 +249,7 @@
 method_setup analz_freshCryptK = \<open>
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
-      (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+      (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
           REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshCryptK_lemma}),
           ALLGOALS (asm_simp_tac
             (put_simpset OtwayReesBella.analz_image_freshK_ss ctxt))])))\<close>
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Public.thy	Sun May 18 14:33:01 2025 +0000
@@ -407,8 +407,8 @@
 
 val analz_image_freshK_ss =
   simpset_of
-   (\<^context> delsimps [image_insert, image_Un]
-    delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
+   (\<^context> delsimps @{thms image_insert image_Un}
+    delsimps @{thms imp_disjL}    (*reduces blow-up*)
     addsimps @{thms analz_image_freshK_simps})
 
 (*Tactic for possibility theorems*)
@@ -433,7 +433,7 @@
 method_setup analz_freshK = \<open>
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
-      (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+      (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
           REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))])))\<close>
     "for proving the Session Key Compromise theorem"
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Shared.thy	Sun May 18 14:33:01 2025 +0000
@@ -218,8 +218,8 @@
 
 val analz_image_freshK_ss =
   simpset_of
-   (\<^context> delsimps [image_insert, image_Un]
-      delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
+   (\<^context> delsimps @{thms image_insert image_Un}
+      delsimps @{thms imp_disjL}    (*reduces blow-up*)
       addsimps @{thms analz_image_freshK_simps})
 
 end
@@ -237,7 +237,7 @@
 method_setup analz_freshK = \<open>
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
-      (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+      (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
           REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (put_simpset Shared.analz_image_freshK_ss ctxt))])))\<close>
     "for proving the Session Key Compromise theorem"
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Auth/Smartcard/ShoupRubin.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sun May 18 14:33:01 2025 +0000
@@ -817,7 +817,7 @@
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST
-       (resolve_tac ctxt [allI, ballI, impI]),
+       (resolve_tac ctxt @{thms allI ballI impI}),
         REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
         ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt
           addsimps [@{thm knows_Spy_Inputs_secureM_sr_Spy},
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Auth/Smartcard/ShoupRubinBella.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sun May 18 14:33:01 2025 +0000
@@ -826,7 +826,7 @@
 method_setup sc_analz_freshK = \<open>
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
-      (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+      (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
           REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt
               addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy},
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Sun May 18 14:33:01 2025 +0000
@@ -383,8 +383,8 @@
 
 val analz_image_freshK_ss = 
   simpset_of
-   (\<^context> delsimps [image_insert, image_Un]
-               delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
+   (\<^context> delsimps @{thms image_insert image_Un}
+               delsimps @{thms imp_disjL}    (*reduces blow-up*)
                addsimps @{thms analz_image_freshK_simps})
 end
 \<close>
@@ -400,7 +400,7 @@
 method_setup analz_freshK = \<open>
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
-      (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+      (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
           REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt))])))\<close>
     "for proving the Session Key Compromise theorem"
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Datatype_Examples/Stream_Processor.thy
--- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Sun May 18 14:33:01 2025 +0000
@@ -150,13 +150,13 @@
       resolve_tac ctxt @{thms relcomppI},
       resolve_tac ctxt @{thms GrpI},
       resolve_tac ctxt [refl],
-      resolve_tac ctxt [CollectI],
+      resolve_tac ctxt @{thms CollectI},
       BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks,
       resolve_tac ctxt @{thms relcomppI}, assume_tac ctxt,
       resolve_tac ctxt @{thms conversepI},
       resolve_tac ctxt @{thms GrpI},
       resolve_tac ctxt [refl],
-      resolve_tac ctxt [CollectI],
+      resolve_tac ctxt @{thms CollectI},
       BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks,
       REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
       hyp_subst_tac ctxt,
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Sun May 18 14:33:01 2025 +0000
@@ -115,7 +115,7 @@
 (**Simp_tacs**)
 
 fun before_set2pred_simp_tac ctxt =
-  simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]);
+  simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm Collect_conj_eq} RS sym, @{thm Compl_Collect}]);
 
 fun split_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]);
@@ -135,9 +135,9 @@
 fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
   before_set2pred_simp_tac ctxt i THEN_MAYBE
   EVERY [
-    resolve_tac ctxt [subsetI] i,
-    resolve_tac ctxt [CollectI] i,
-    dresolve_tac ctxt [CollectD] i,
+    resolve_tac ctxt @{thms subsetI} i,
+    resolve_tac ctxt @{thms CollectI} i,
+    dresolve_tac ctxt @{thms CollectD} i,
     TRY (split_all_tac ctxt i) THEN_MAYBE
      (rename_tac var_names i THEN
       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
@@ -151,13 +151,13 @@
 (*******************************************************************************)
 
 fun max_simp_tac ctxt var_names tac =
-  FIRST' [resolve_tac ctxt [subset_refl],
+  FIRST' [resolve_tac ctxt @{thms subset_refl},
     set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
 
 fun basic_simp_tac ctxt var_names tac =
   simp_tac
     (put_simpset HOL_basic_ss ctxt
-      addsimps [mem_Collect_eq, @{thm split_conv}] |> Simplifier.add_proc Record.simproc)
+      addsimps @{thms mem_Collect_eq split_conv} |> Simplifier.add_proc Record.simproc)
   THEN_MAYBE' max_simp_tac ctxt var_names tac;
 
 
@@ -189,7 +189,7 @@
             rule_tac true (i + 1)]]
          THEN (
            if pre_cond then basic_simp_tac ctxt var_names tac i
-           else resolve_tac ctxt [subset_refl] i)));
+           else resolve_tac ctxt @{thms subset_refl} i)));
   in rule_tac end;
 
 
@@ -227,7 +227,7 @@
             rule_tac true (i + 1)]]
          THEN (
            if pre_cond then basic_simp_tac ctxt var_names tac i
-           else resolve_tac ctxt [subset_refl] i)));
+           else resolve_tac ctxt @{thms subset_refl} i)));
   in rule_tac end;
 
 
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Hoare_Parallel/Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Sun May 18 14:33:01 2025 +0000
@@ -777,12 +777,12 @@
 apply(tactic \<open>TRYALL (eresolve_tac \<^context> [disjE])\<close>)
 apply simp_all
 apply(tactic \<open>TRYALL(EVERY'[resolve_tac \<^context> [disjI2],
-    resolve_tac \<^context> [subset_trans],
+    resolve_tac \<^context> @{thms subset_trans},
     eresolve_tac \<^context> @{thms Graph3},
     force_tac \<^context>,
     assume_tac \<^context>])\<close>)
 apply(tactic \<open>TRYALL(EVERY'[resolve_tac \<^context> [disjI2],
-    eresolve_tac \<^context> [subset_trans],
+    eresolve_tac \<^context> @{thms subset_trans},
     resolve_tac \<^context> @{thms Graph9},
     force_tac \<^context>])\<close>)
 apply(tactic \<open>TRYALL(EVERY'[resolve_tac \<^context> [disjI1],
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Sun May 18 14:33:01 2025 +0000
@@ -1188,7 +1188,7 @@
 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
 \<comment> \<open>35 subgoals left\<close>
 apply(tactic \<open>TRYALL(EVERY'[resolve_tac \<^context> [disjI1],
-    resolve_tac \<^context> [subset_trans],
+    resolve_tac \<^context> @{thms subset_trans},
     eresolve_tac \<^context> @{thms Graph3},
     force_tac \<^context>,
     assume_tac \<^context>])\<close>)
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun May 18 14:33:01 2025 +0000
@@ -133,7 +133,7 @@
 val at_fin_set_fresh = @{thm at_fin_set_fresh};
 val abs_fun_eq1 = @{thm abs_fun_eq1};
 
-fun collect_simp ctxt = rewrite_rule ctxt [mk_meta_eq mem_Collect_eq];
+fun collect_simp ctxt = rewrite_rule ctxt [mk_meta_eq @{thm mem_Collect_eq}];
 
 fun mk_perm Ts t u =
   let
@@ -587,7 +587,7 @@
                Const (cname, U --> HOLogic.boolT)) NONE
             (fn ctxt =>
               resolve_tac ctxt [exI] 1 THEN
-              resolve_tac ctxt [CollectI] 1 THEN
+              resolve_tac ctxt @{thms CollectI} 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)
               (resolve_tac ctxt rep_intrs 1))) thy |> (fn ((_, r), thy) =>
         let
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Sun May 18 14:33:01 2025 +0000
@@ -848,7 +848,7 @@
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
          (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
-          (insert_commute RS ssubst) 1),
+          (@{thm insert_commute} RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ctxt 1,
        REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Set.thy	Sun May 18 14:33:01 2025 +0000
@@ -2027,59 +2027,4 @@
 lemmas set_mp = subsetD
 lemmas set_rev_mp = rev_subsetD
 
-ML \<open>
-val Ball_def = @{thm Ball_def}
-val Bex_def = @{thm Bex_def}
-val CollectD = @{thm CollectD}
-val CollectE = @{thm CollectE}
-val CollectI = @{thm CollectI}
-val Collect_conj_eq = @{thm Collect_conj_eq}
-val Collect_mem_eq = @{thm Collect_mem_eq}
-val IntD1 = @{thm IntD1}
-val IntD2 = @{thm IntD2}
-val IntE = @{thm IntE}
-val IntI = @{thm IntI}
-val Int_Collect = @{thm Int_Collect}
-val UNIV_I = @{thm UNIV_I}
-val UNIV_witness = @{thm UNIV_witness}
-val UnE = @{thm UnE}
-val UnI1 = @{thm UnI1}
-val UnI2 = @{thm UnI2}
-val ballE = @{thm ballE}
-val ballI = @{thm ballI}
-val bexCI = @{thm bexCI}
-val bexE = @{thm bexE}
-val bexI = @{thm bexI}
-val bex_triv = @{thm bex_triv}
-val bspec = @{thm bspec}
-val contra_subsetD = @{thm contra_subsetD}
-val equalityCE = @{thm equalityCE}
-val equalityD1 = @{thm equalityD1}
-val equalityD2 = @{thm equalityD2}
-val equalityE = @{thm equalityE}
-val equalityI = @{thm equalityI}
-val imageE = @{thm imageE}
-val imageI = @{thm imageI}
-val image_Un = @{thm image_Un}
-val image_insert = @{thm image_insert}
-val insert_commute = @{thm insert_commute}
-val insert_iff = @{thm insert_iff}
-val mem_Collect_eq = @{thm mem_Collect_eq}
-val rangeE = @{thm rangeE}
-val rangeI = @{thm rangeI}
-val range_eqI = @{thm range_eqI}
-val subsetCE = @{thm subsetCE}
-val subsetD = @{thm subsetD}
-val subsetI = @{thm subsetI}
-val subset_refl = @{thm subset_refl}
-val subset_trans = @{thm subset_trans}
-val vimageD = @{thm vimageD}
-val vimageE = @{thm vimageE}
-val vimageI = @{thm vimageI}
-val vimageI2 = @{thm vimageI2}
-val vimage_Collect = @{thm vimage_Collect}
-val vimage_Int = @{thm vimage_Int}
-val vimage_Un = @{thm vimage_Un}
-\<close>
-
 end
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sun May 18 14:33:01 2025 +0000
@@ -868,7 +868,7 @@
        else inter (op =) repTA_tfrees all_TA_params_in_order);
     val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
       maybe_typedef force_out_of_line (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
-        (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+        (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
 
     val repTB = mk_T_of_bnf Ds Bs bnf;
     val TB = Term.typ_subst_atomic (As ~~ Bs) TA;
@@ -900,7 +900,7 @@
 
     val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
       maybe_typedef false (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE
-        (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+        (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
 
     val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite, bd_regularCard) =
       if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl},
@@ -930,7 +930,7 @@
     fun map_cong0_tac ctxt =
       EVERY' (rtac ctxt @{thm type_copy_map_cong0} :: rtac ctxt (map_cong0_of_bnf bnf) ::
         map (fn i => EVERY' [select_prem_tac ctxt live (dtac ctxt meta_spec) i, etac ctxt meta_mp,
-          etac ctxt (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1;
+          etac ctxt (o_apply RS @{thm equalityD2} RS set_mp)]) (1 upto live)) 1;
     fun set_map0_tac thm ctxt =
       rtac ctxt (@{thm type_copy_set_map0} OF [type_definition, thm]) 1;
     val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt (@{thm ordLess_ordIso_trans} OF
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/BNF/bnf_comp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Sun May 18 14:33:01 2025 +0000
@@ -98,11 +98,11 @@
       EVERY' (map_index (fn (i, map_cong0) =>
         rtac ctxt map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) =>
           EVERY' [select_prem_tac ctxt n (dtac ctxt @{thm meta_spec}) (k + 1), etac ctxt meta_mp,
-            rtac ctxt (equalityD2 RS set_mp), rtac ctxt (set_alt RS fun_cong RS trans),
+            rtac ctxt (@{thm equalityD2} RS set_mp), rtac ctxt (set_alt RS fun_cong RS trans),
             rtac ctxt trans_o_apply, rtac ctxt (@{thm collect_def} RS arg_cong_Union),
             rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I},
             REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1},
-            rtac ctxt (o_apply RS equalityD2 RS set_mp), etac ctxt @{thm imageI}, assume_tac ctxt])
+            rtac ctxt (o_apply RS @{thm equalityD2} RS set_mp), etac ctxt @{thm imageI}, assume_tac ctxt])
           comp_set_alts))
       map_cong0s) 1)
   end;
@@ -211,7 +211,7 @@
   unfold_thms_tac ctxt comp_wit_thms THEN
   REPEAT_DETERM ((assume_tac ctxt ORELSE'
     REPEAT_DETERM o eresolve_tac ctxt @{thms UnionE UnE} THEN'
-    etac ctxt imageE THEN' TRY o dresolve_tac ctxt Gwit_thms THEN'
+    etac ctxt @{thm imageE} THEN' TRY o dresolve_tac ctxt Gwit_thms THEN'
     (etac ctxt FalseE ORELSE'
     hyp_subst_tac ctxt THEN'
     dresolve_tac ctxt Fwit_thms THEN'
@@ -232,7 +232,7 @@
   (rtac ctxt subset_UNIV ORELSE' assume_tac ctxt) 1 THEN
   REPEAT_DETERM (CHANGED (etac ctxt conjE 1)) THEN
   REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE' assume_tac ctxt) 1))) ORELSE
-  ((rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN
+  ((rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt @{thm CollectI}) 1 THEN
     REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt subset_UNIV 1));
 
 
@@ -251,7 +251,7 @@
   REPEAT_DETERM (CHANGED ((etac ctxt conjI ORELSE'
     rtac ctxt conjI THEN' rtac ctxt @{thm empty_subsetI}) 1)) THEN
   (rtac ctxt @{thm empty_subsetI} ORELSE' assume_tac ctxt) 1) ORELSE
-  ((rtac ctxt sym THEN' rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt CollectI) 1 THEN
+  ((rtac ctxt sym THEN' rtac ctxt @{thm UNIV_eq_I} THEN' rtac ctxt @{thm CollectI}) 1 THEN
     REPEAT_DETERM (TRY (rtac ctxt conjI 1) THEN rtac ctxt @{thm empty_subsetI} 1));
 
 
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun May 18 14:33:01 2025 +0000
@@ -2038,7 +2038,7 @@
     val consumes_attr = Attrib.consumes 1;
   in
     map (mk_thm ctxt fpTs ctrss
-        #> nn = 1 ? map_prod (fn thm => rotate_prems ~1 (thm RS bspec)) (cons consumes_attr))
+        #> nn = 1 ? map_prod (fn thm => rotate_prems ~1 (thm RS @{thm bspec})) (cons consumes_attr))
       (transpose setss)
   end;
 
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun May 18 14:33:01 2025 +0000
@@ -506,7 +506,7 @@
     live_nesting_set_maps @ extra_unfolds @ basic_sumprod_thms_set @
     @{thms UN_UN_flatten UN_Un_distrib UN_Un sup_assoc[THEN sym]}) THEN
   ALLGOALS (rtac ctxt @{thm set_eqI[OF iffI]}) THEN
-  ALLGOALS (REPEAT_DETERM o etac ctxt UnE) THEN
+  ALLGOALS (REPEAT_DETERM o etac ctxt @{thm UnE}) THEN
   ALLGOALS (REPEAT o resolve_tac ctxt @{thms UnI1 UnI2} THEN' assume_tac ctxt);
 
 fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Sun May 18 14:33:01 2025 +0000
@@ -238,7 +238,7 @@
 
     val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
     val in_mono'_thms = map (fn thm =>
-      (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
+      (thm OF (replicate m @{thm subset_refl})) RS @{thm set_mp}) in_monos;
 
     val map_arg_cong_thms =
       let
@@ -306,7 +306,7 @@
     val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
 
     val coalg_in_thms = map (fn i =>
-      coalg_def RS iffD1 RS mk_conjunctN n i RS bspec) ks
+      coalg_def RS iffD1 RS mk_conjunctN n i RS @{thm bspec}) ks
 
     val coalg_set_thmss =
       let
@@ -336,7 +336,7 @@
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => (rtac ctxt (coalg_def RS iffD2) 1 THEN CONJ_WRAP
-            (K (EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
+            (K (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm CollectI},
               CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm subset_UNIV}])) allAs] 1)) ss))
         |> Thm.close_derivation \<^here>
       end;
@@ -423,7 +423,7 @@
         (map prove image_goals, map prove elim_goals)
       end;
 
-    val mor_image'_thms = map (fn thm => @{thm set_mp} OF [thm, imageI]) mor_image_thms;
+    val mor_image'_thms = map (fn thm => @{thm set_mp} OF [thm, @{thm imageI}]) mor_image_thms;
 
     val mor_incl_thm =
       let
@@ -436,7 +436,7 @@
         |> Thm.close_derivation \<^here>
       end;
 
-    val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
+    val mor_id_thm = mor_incl_thm OF (replicate n @{thm subset_refl});
 
     val mor_comp_thm =
       let
@@ -757,7 +757,7 @@
           val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
             typedef (sbdT_bind, sum_bdT_params', NoSyn)
               (HOLogic.mk_UNIV sum_bdT) NONE (fn ctxt =>
-                EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+                EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
 
           val sbdT = Type (sbdT_name, sum_bdT_params);
           val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
@@ -1341,7 +1341,7 @@
       |> Thm.close_derivation \<^here>;
 
     val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
-    val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, UNIV_I]) mor_image'_thms;
+    val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, @{thm UNIV_I}]) mor_image'_thms;
 
     val timer = time (timer "Final coalgebra");
 
@@ -1467,7 +1467,7 @@
     val mor_unfold_thm =
       let
         val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
-        val morEs' = map (fn thm => (thm OF [mor_final_thm, UNIV_I]) RS sym) morE_thms;
+        val morEs' = map (fn thm => (thm OF [mor_final_thm, @{thm UNIV_I}]) RS sym) morE_thms;
         val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks));
         val vars = Variable.add_free_names lthy goal [];
       in
@@ -1476,7 +1476,7 @@
             unfold_defs Abs_inverses' morEs' map_comp_id_thms map_cong0s)
         |> Thm.close_derivation \<^here>
       end;
-    val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
+    val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, @{thm UNIV_I}]) RS sym) morE_thms;
 
     val (raw_coind_thms, raw_coind_thm) =
       let
@@ -2008,7 +2008,7 @@
               ((set_minimal
                 |> Thm.instantiate' cTs (mk_induct_tinst phis jsets y y')
                 |> unfold_thms lthy incls) OF
-                (replicate n ballI @
+                (replicate n @{thm ballI} @
                   maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
               |> singleton (Proof_Context.export names_lthy lthy)
               |> rule_by_tactic lthy (ALLGOALS (TRY o etac lthy asm_rl)))
@@ -2049,7 +2049,7 @@
                 |> Thm.close_derivation \<^here>))
               ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss'
           in
-            map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss
+            map2 (map2 (fn le => fn ge => @{thm equalityI} OF [le, ge])) set_le_thmss set_ge_thmss
             |> `transpose
           end;
 
@@ -2451,7 +2451,7 @@
             goals dtor_Jset_induct_thms
             |> map split_conj_thm
             |> transpose
-            |> map (map_filter (try (fn thm => thm RS bspec RS mp)))
+            |> map (map_filter (try (fn thm => thm RS @{thm bspec} RS mp)))
             |> curry op ~~ (map_index Library.I (map (close_wit I) wits))
             |> filter (fn (_, thms) => length thms = m)
           end;
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sun May 18 14:33:01 2025 +0000
@@ -108,7 +108,7 @@
 val sum_case_cong_weak = @{thm sum.case_cong_weak};
 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
 val Collect_splitD_set_mp = @{thm Collect_case_prodD[OF set_mp]};
-val rev_bspec = Drule.rotate_prems 1 bspec;
+val rev_bspec = Drule.rotate_prems 1 @{thm bspec};
 val Un_cong = @{thm arg_cong2[of _ _ _ _ "(\<union>)"]};
 val converse_shift = @{thm converse_subset_swap} RS iffD1;
 
@@ -116,29 +116,29 @@
   dtac ctxt (coalg_def RS iffD1) 1 THEN
   REPEAT_DETERM (etac ctxt conjE 1) THEN
   EVERY' [dtac ctxt rev_bspec, assume_tac ctxt] 1 THEN
-  REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN assume_tac ctxt 1;
+  REPEAT_DETERM (eresolve_tac ctxt @{thms CollectE conjE} 1) THEN assume_tac ctxt 1;
 
 fun mk_mor_elim_tac ctxt mor_def =
   (dtac ctxt (mor_def RS iffD1) THEN'
   REPEAT o etac ctxt conjE THEN'
   TRY o rtac ctxt @{thm image_subsetI} THEN'
-  etac ctxt bspec THEN'
+  etac ctxt @{thm bspec} THEN'
   assume_tac ctxt) 1;
 
 fun mk_mor_incl_tac ctxt mor_def map_ids =
   (rtac ctxt (mor_def RS iffD2) THEN'
   rtac ctxt conjI THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
+  CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
     map_ids THEN'
   CONJ_WRAP' (fn thm =>
-    (EVERY' [rtac ctxt ballI, rtac ctxt (thm RS trans), rtac ctxt sym, rtac ctxt (id_apply RS arg_cong)])) map_ids) 1;
+    (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (thm RS trans), rtac ctxt sym, rtac ctxt (id_apply RS arg_cong)])) map_ids) 1;
 
 fun mk_mor_comp_tac ctxt mor_def mor_images morEs map_comp_ids =
   let
-    fun fbetw_tac image = EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt image,
+    fun fbetw_tac image = EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt image,
       etac ctxt image, assume_tac ctxt];
     fun mor_tac ((mor_image, morE), map_comp_id) =
-      EVERY' [rtac ctxt ballI, stac ctxt o_apply, rtac ctxt trans, rtac ctxt (map_comp_id RS sym), rtac ctxt trans,
+      EVERY' [rtac ctxt @{thm ballI}, stac ctxt o_apply, rtac ctxt trans, rtac ctxt (map_comp_id RS sym), rtac ctxt trans,
         etac ctxt (morE RS arg_cong), assume_tac ctxt, etac ctxt morE,
         etac ctxt mor_image, assume_tac ctxt];
   in
@@ -151,24 +151,24 @@
   let
     val n = length morEs;
     fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE,
-      rtac ctxt UNIV_I, rtac ctxt sym, rtac ctxt o_apply];
+      rtac ctxt @{thm UNIV_I}, rtac ctxt sym, rtac ctxt o_apply];
   in
     EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs,
-    rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs,
+    rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' rtac ctxt @{thm UNIV_I})) morEs,
     CONJ_WRAP' (fn i =>
-      EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt ballI, etac ctxt @{thm comp_eq_dest}]) (1 upto n)] 1
+      EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt @{thm ballI}, etac ctxt @{thm comp_eq_dest}]) (1 upto n)] 1
   end;
 
 fun mk_mor_str_tac ctxt ks mor_UNIV =
   (rtac ctxt (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac ctxt refl)) ks) 1;
 
 fun mk_set_incl_Jset_tac ctxt rec_Suc =
-  EVERY' (map (rtac ctxt) [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym,
-    rec_Suc]) 1;
+  EVERY' (map (rtac ctxt) (@{thms SUP_upper2 UNIV_I ord_le_eq_trans Un_upper1 sym} @
+    [rec_Suc])) 1;
 
 fun mk_set_Jset_incl_Jset_tac ctxt n rec_Suc i =
-  EVERY' (map (rtac ctxt) [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2,
-    rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;
+  EVERY' (map (rtac ctxt) (@{thms UN_least subsetI UN_I UNIV_I set_mp equalityD2} @
+    [rec_Suc, @{thm UnI2}, mk_UnIN n i]) @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;
 
 fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs =
   EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
@@ -182,7 +182,7 @@
         else (rtac ctxt @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
         CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
           (K (EVERY' [rtac ctxt @{thm UN_least}, REPEAT_DETERM o eresolve_tac ctxt [allE, conjE],
-            rtac ctxt subset_trans, assume_tac ctxt, Goal.assume_rule_tac ctxt])) rec_0s])
+            rtac ctxt @{thm subset_trans}, assume_tac ctxt, Goal.assume_rule_tac ctxt])) rec_0s])
       rec_Sucs] 1;
 
 fun mk_Jset_minimal_tac ctxt n col_minimal =
@@ -221,18 +221,18 @@
 
     fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
       EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, dtac ctxt (mk_conjunctN n i),
-        etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt bexE,
-        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
+        etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt @{thm bexE},
+        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
         rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI),
         CONJ_WRAP' (fn thm => EVERY' [rtac ctxt trans, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt map_cong0,
           REPEAT_DETERM_N m o rtac ctxt thm, REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
           assume_tac ctxt])
         @{thms fst_diag_id snd_diag_id},
-        rtac ctxt CollectI,
+        rtac ctxt @{thm CollectI},
         CONJ_WRAP' (fn (i, thm) =>
           if i <= m
-          then EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans,
-            etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
+          then EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm subset_trans},
+            etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI},
             rtac ctxt @{thm case_prodI}, rtac ctxt refl]
           else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
             rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_case_prod_in_rel_leI}])
@@ -242,9 +242,9 @@
       EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
         etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
         dtac ctxt (in_rel RS @{thm iffD1}),
-        REPEAT_DETERM o eresolve_tac ctxt ([CollectE, conjE, exE] @
-          @{thms CollectE Collect_case_prod_in_rel_leE}),
-        rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
+        REPEAT_DETERM o eresolve_tac ctxt
+          @{thms CollectE conjE exE CollectE Collect_case_prod_in_rel_leE},
+        rtac ctxt @{thm bexI}, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
         REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
         REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
         assume_tac ctxt, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
@@ -253,7 +253,7 @@
         rtac ctxt trans, rtac ctxt map_cong0,
         REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_case_prodD}, etac ctxt set_mp, assume_tac ctxt],
         REPEAT_DETERM_N n o rtac ctxt refl,
-        assume_tac ctxt, rtac ctxt CollectI,
+        assume_tac ctxt, rtac ctxt @{thm CollectI},
         CONJ_WRAP' (fn (i, thm) =>
           if i <= m then rtac ctxt subset_UNIV
           else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
@@ -268,8 +268,8 @@
 fun mk_bis_converse_tac ctxt m bis_rel rel_congs rel_converseps =
   EVERY' [rtac ctxt (bis_rel RS iffD2), dtac ctxt (bis_rel RS iffD1),
     REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI,
-    CONJ_WRAP' (K (EVERY' [rtac ctxt converse_shift, etac ctxt subset_trans,
-      rtac ctxt equalityD2, rtac ctxt @{thm converse_Times}])) rel_congs,
+    CONJ_WRAP' (K (EVERY' [rtac ctxt converse_shift, etac ctxt @{thm subset_trans},
+      rtac ctxt @{thm equalityD2}, rtac ctxt @{thm converse_Times}])) rel_congs,
     CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
       EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
         rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
@@ -312,13 +312,13 @@
     unfold_thms_tac ctxt [bis_def] THEN
     EVERY' [rtac ctxt conjI,
       CONJ_WRAP' (fn i =>
-        EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt bspec, assume_tac ctxt,
+        EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt @{thm bspec}, assume_tac ctxt,
           dtac ctxt conjunct1, etac ctxt (mk_conjunctN n i)]) ks,
       CONJ_WRAP' (fn (i, in_mono) =>
         EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, etac ctxt @{thm UN_E},
-          dtac ctxt bspec, assume_tac ctxt,
+          dtac ctxt @{thm bspec}, assume_tac ctxt,
           dtac ctxt conjunct2, dtac ctxt (mk_conjunctN n i), etac ctxt allE, etac ctxt allE, dtac ctxt mp,
-          assume_tac ctxt, etac ctxt bexE, rtac ctxt bexI, assume_tac ctxt, rtac ctxt in_mono,
+          assume_tac ctxt, etac ctxt @{thm bexE}, rtac ctxt @{thm bexI}, assume_tac ctxt, rtac ctxt in_mono,
           REPEAT_DETERM_N n o etac ctxt @{thm SUP_upper2[OF _ subset_refl]},
           assume_tac ctxt]) (ks ~~ in_monos)] 1
   end;
@@ -328,14 +328,14 @@
     val n = length lsbis_defs;
   in
     EVERY' [rtac ctxt (Thm.permute_prems 0 1 bis_cong), EVERY' (map (rtac ctxt) lsbis_defs),
-      rtac ctxt bis_Union, rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, exE],
+      rtac ctxt bis_Union, rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE exE},
       hyp_subst_tac ctxt, etac ctxt bis_cong, EVERY' (map (rtac ctxt o mk_nth_conv n) (1 upto n))] 1
   end;
 
 fun mk_incl_lsbis_tac ctxt n i lsbis_def =
-  EVERY' [rtac ctxt @{thm xt1(3)}, rtac ctxt lsbis_def, rtac ctxt @{thm SUP_upper2}, rtac ctxt CollectI,
+  EVERY' [rtac ctxt @{thm xt1(3)}, rtac ctxt lsbis_def, rtac ctxt @{thm SUP_upper2}, rtac ctxt @{thm CollectI},
     REPEAT_DETERM_N n o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
-    rtac ctxt equalityD2, rtac ctxt (mk_nth_conv n i)] 1;
+    rtac ctxt @{thm equalityD2}, rtac ctxt (mk_nth_conv n i)] 1;
 
 fun mk_equiv_lsbis_tac ctxt sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
   EVERY' [rtac ctxt @{thm equivI},
@@ -359,26 +359,26 @@
     val n = length strT_defs;
     val ks = 1 upto n;
     fun coalg_tac (i, (active_sets, def)) =
-      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE],
+      EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE},
         hyp_subst_tac ctxt, rtac ctxt (def RS trans RS @{thm ssubst_mem}), etac ctxt (arg_cong RS trans),
-        rtac ctxt (mk_sum_caseN n i), rtac ctxt CollectI,
+        rtac ctxt (mk_sum_caseN n i), rtac ctxt @{thm CollectI},
         REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV],
         CONJ_WRAP' (fn (i, thm) => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
-          rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt exI, rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
+          rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt exI, rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
           rtac ctxt conjI,
           rtac ctxt conjI, etac ctxt @{thm empty_Shift}, dtac ctxt set_rev_mp,
-            etac ctxt equalityD1, etac ctxt CollectD,
-          rtac ctxt ballI,
-            CONJ_WRAP' (fn i => EVERY' [rtac ctxt ballI, etac ctxt CollectE, dtac ctxt @{thm ShiftD},
-              dtac ctxt bspec, etac ctxt thin_rl, assume_tac ctxt, dtac ctxt (mk_conjunctN n i),
-              dtac ctxt bspec, rtac ctxt CollectI, etac ctxt @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
+            etac ctxt @{thm equalityD1}, etac ctxt @{thm CollectD},
+          rtac ctxt @{thm ballI},
+            CONJ_WRAP' (fn i => EVERY' [rtac ctxt @{thm ballI}, etac ctxt @{thm CollectE}, dtac ctxt @{thm ShiftD},
+              dtac ctxt @{thm bspec}, etac ctxt thin_rl, assume_tac ctxt, dtac ctxt (mk_conjunctN n i),
+              dtac ctxt @{thm bspec}, rtac ctxt @{thm CollectI}, etac ctxt @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
               REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
               rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
               rtac ctxt (@{thm append_Cons} RS sym RS arg_cong RS trans), assume_tac ctxt,
               CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong},
                 rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift},
                 rtac ctxt (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
-          dtac ctxt bspec, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), dtac ctxt bspec,
+          dtac ctxt @{thm bspec}, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), dtac ctxt @{thm bspec},
           etac ctxt @{thm set_mp[OF equalityD1]}, assume_tac ctxt,
           REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
           rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
@@ -400,14 +400,14 @@
     EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac ctxt allI,
       CONJ_WRAP' (fn Lev_0 =>
-        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
+        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS @{thm equalityD1} RS set_mp),
           etac ctxt @{thm singletonE}, etac ctxt ssubst, rtac ctxt @{thm list.size(3)}]) Lev_0s,
       REPEAT_DETERM o rtac ctxt allI,
       CONJ_WRAP' (fn Lev_Suc =>
-        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp),
-          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
+        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp),
+          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
             (fn i =>
-              EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt,
+              EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE}, hyp_subst_tac ctxt,
                 rtac ctxt trans, rtac ctxt @{thm length_Cons}, rtac ctxt @{thm arg_cong[of _ _ Suc]},
                 REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i),
                 etac ctxt mp, assume_tac ctxt]) ks])
@@ -450,16 +450,16 @@
     EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac ctxt allI,
       CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
-        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
+        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS @{thm equalityD1} RS set_mp),
           etac ctxt @{thm singletonE}, hyp_subst_tac ctxt,
           CONJ_WRAP' (fn i' => rtac ctxt impI THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN'
             (if i = i'
             then EVERY' [dtac ctxt (mk_InN_inject n i), hyp_subst_tac ctxt,
               CONJ_WRAP' (fn (i'', Lev_0'') =>
                 EVERY' [rtac ctxt impI, rtac ctxt @{thm ssubst_mem[OF append_Nil]},
-                  rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i''),
-                  rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
-                  etac ctxt conjI, rtac ctxt (Lev_0'' RS equalityD2 RS set_mp),
+                  rtac ctxt (Lev_Suc RS @{thm equalityD2} RS set_mp), rtac ctxt (mk_UnIN n i''),
+                  rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
+                  etac ctxt conjI, rtac ctxt (Lev_0'' RS @{thm equalityD2} RS set_mp),
                   rtac ctxt @{thm singletonI}])
               (ks ~~ Lev_0s)]
             else etac ctxt (mk_InN_not_InM i' i RS notE)))
@@ -467,15 +467,15 @@
       ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
       REPEAT_DETERM o rtac ctxt allI,
       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
-        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp),
-          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
+        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp),
+          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
             (fn (i, from_to_sbd) =>
-              EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt,
+              EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE}, hyp_subst_tac ctxt,
                 CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
                   CONJ_WRAP' (fn i'' =>
-                    EVERY' [rtac ctxt impI, rtac ctxt (Lev_Suc RS equalityD2 RS set_mp),
+                    EVERY' [rtac ctxt impI, rtac ctxt (Lev_Suc RS @{thm equalityD2} RS set_mp),
                       rtac ctxt @{thm ssubst_mem[OF append_Cons]}, rtac ctxt (mk_UnIN n i),
-                      rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
+                      rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
                       rtac ctxt conjI, assume_tac ctxt, dtac ctxt (sym RS trans RS sym),
                       rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans),
                       etac ctxt (from_to_sbd RS arg_cong), REPEAT_DETERM o etac ctxt allE,
@@ -496,19 +496,19 @@
     EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac ctxt allI,
       CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
-        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
+        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS @{thm equalityD1} RS set_mp),
           etac ctxt @{thm singletonE}, hyp_subst_tac ctxt,
           CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
             CONJ_WRAP' (fn i'' => rtac ctxt impI  THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN'
               (if i = i''
               then EVERY' [dtac ctxt @{thm ssubst_mem[OF sym[OF append_Nil]]},
-                dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), dtac ctxt (mk_InN_inject n i),
+                dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp), dtac ctxt (mk_InN_inject n i),
                 hyp_subst_tac ctxt,
-                CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
-                  (fn k => REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN'
+                CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
+                  (fn k => REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE} THEN'
                     dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN'
                     (if k = i'
-                    then EVERY' [dtac ctxt (mk_InN_inject n k), hyp_subst_tac ctxt, etac ctxt imageI]
+                    then EVERY' [dtac ctxt (mk_InN_inject n k), hyp_subst_tac ctxt, etac ctxt @{thm imageI}]
                     else etac ctxt (mk_InN_not_InM i' k RS notE)))
                 (rev ks)]
               else etac ctxt (mk_InN_not_InM i'' i RS notE)))
@@ -517,15 +517,15 @@
       ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
       REPEAT_DETERM o rtac ctxt allI,
       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
-        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp),
-          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
+        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp),
+          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE}))
             (fn (i, (from_to_sbd, to_sbd_inj)) =>
-              REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
+              REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE} THEN' hyp_subst_tac ctxt THEN'
               CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
                 dtac ctxt @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
-                dtac ctxt (Lev_Suc RS equalityD1 RS set_mp) THEN'
-                CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) (fn k =>
-                  REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN'
+                dtac ctxt (Lev_Suc RS @{thm equalityD1} RS set_mp) THEN'
+                CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE})) (fn k =>
+                  REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE} THEN'
                   dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN'
                   (if k = i
                   then EVERY' [dtac ctxt (mk_InN_inject n i),
@@ -556,26 +556,26 @@
 
     fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, ((length_Lev, length_Lev'),
       (rv_lasts, (set_map0s, (set_Levss, set_image_Levss))))))))) =
-      EVERY' [rtac ctxt ballI, rtac ctxt (carT_def RS equalityD2 RS set_mp),
-        rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, rtac ctxt conjI,
+      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (carT_def RS @{thm equalityD2} RS set_mp),
+        rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, rtac ctxt conjI,
         rtac ctxt conjI,
-          rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt (Lev_0 RS equalityD2 RS set_mp),
+          rtac ctxt @{thm UN_I}, rtac ctxt @{thm UNIV_I}, rtac ctxt (Lev_0 RS @{thm equalityD2} RS set_mp),
           rtac ctxt @{thm singletonI},
         (**)
-          rtac ctxt ballI, etac ctxt @{thm UN_E},
+          rtac ctxt @{thm ballI}, etac ctxt @{thm UN_E},
           CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
             (set_Levs, set_image_Levs))))) =>
-            EVERY' [rtac ctxt ballI,
-              REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
+            EVERY' [rtac ctxt @{thm ballI},
+              REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE SuccE UN_E},
               rtac ctxt (rev_mp OF [rv_last, impI]), etac ctxt exE, rtac ctxt (isNode_def RS iffD2),
               rtac ctxt exI, rtac ctxt conjI,
               if n = 1 then rtac ctxt refl
               else etac ctxt (sum_case_cong_weak RS trans) THEN' rtac ctxt (mk_sum_caseN n i),
               CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
-                EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI},
-                  rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, etac ctxt set_Lev,
-                  if n = 1 then rtac ctxt refl else assume_tac ctxt, assume_tac ctxt, rtac ctxt subsetI,
-                  REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
+                EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt @{thm equalityI}, rtac ctxt @{thm image_subsetI},
+                  rtac ctxt @{thm CollectI}, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt @{thm UNIV_I}, etac ctxt set_Lev,
+                  if n = 1 then rtac ctxt refl else assume_tac ctxt, assume_tac ctxt, rtac ctxt @{thm subsetI},
+                  REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE SuccE UN_E},
                   REPEAT_DETERM_N 4 o etac ctxt thin_rl,
                   rtac ctxt set_image_Lev,
                   assume_tac ctxt, dtac ctxt length_Lev, hyp_subst_tac ctxt, dtac ctxt length_Lev',
@@ -590,12 +590,12 @@
             (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
           if n = 1 then rtac ctxt refl else rtac ctxt (mk_sum_caseN n i),
           CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
-            EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI},
-              rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt set_Lev,
-              rtac ctxt (Lev_0 RS equalityD2 RS set_mp), rtac ctxt @{thm singletonI}, rtac ctxt rv_Nil,
-              assume_tac ctxt, rtac ctxt subsetI,
-              REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
-              rtac ctxt set_image_Lev, rtac ctxt (Lev_0 RS equalityD2 RS set_mp),
+            EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt @{thm equalityI}, rtac ctxt @{thm image_subsetI},
+              rtac ctxt @{thm CollectI}, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt @{thm UNIV_I}, rtac ctxt set_Lev,
+              rtac ctxt (Lev_0 RS @{thm equalityD2} RS set_mp), rtac ctxt @{thm singletonI}, rtac ctxt rv_Nil,
+              assume_tac ctxt, rtac ctxt @{thm subsetI},
+              REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE SuccE UN_E},
+              rtac ctxt set_image_Lev, rtac ctxt (Lev_0 RS @{thm equalityD2} RS set_mp),
               rtac ctxt @{thm singletonI}, dtac ctxt length_Lev',
               etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF
                 trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
@@ -604,7 +604,7 @@
 
     fun mor_tac (i, (strT_def, ((Lev_Suc, (rv_Nil, rv_Cons)),
       ((map_comp_id, map_cong0), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
-      EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt strT_def,
+      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt sym, rtac ctxt trans, rtac ctxt strT_def,
         CONVERSION (Conv.top_conv
           (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
         if n = 1 then K all_tac
@@ -614,20 +614,20 @@
         EVERY' (@{map 3} (fn i' => fn to_sbd_inj => fn from_to_sbd =>
           DETERM o EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt prod_injectI, rtac ctxt conjI,
             rtac ctxt trans, rtac ctxt @{thm Shift_def},
-            rtac ctxt equalityI, rtac ctxt subsetI, etac ctxt thin_rl,
-            REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm UN_E}], dtac ctxt length_Lev', dtac ctxt asm_rl,
+            rtac ctxt @{thm equalityI}, rtac ctxt @{thm subsetI}, etac ctxt thin_rl,
+            REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE UN_E}, dtac ctxt length_Lev', dtac ctxt asm_rl,
             etac ctxt thin_rl, dtac ctxt @{thm set_rev_mp[OF _ equalityD1]},
             rtac ctxt (@{thm length_Cons} RS arg_cong RS trans), rtac ctxt Lev_Suc,
-            CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) (fn i'' =>
-              EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE],
+            CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 @{thm UnE})) (fn i'' =>
+              EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE},
                 dtac ctxt list_inject_iffD1, etac ctxt conjE,
                 if i' = i'' then EVERY' [dtac ctxt (mk_InN_inject n i'),
                   dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                   assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt, etac ctxt @{thm UN_I[OF UNIV_I]}]
                 else etac ctxt (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
-            rtac ctxt @{thm UN_least}, rtac ctxt subsetI, rtac ctxt CollectI, rtac ctxt @{thm UN_I[OF UNIV_I]},
-            rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i'), rtac ctxt CollectI,
+            rtac ctxt @{thm UN_least}, rtac ctxt @{thm subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm UN_I[OF UNIV_I]},
+            rtac ctxt (Lev_Suc RS @{thm equalityD2} RS set_mp), rtac ctxt (mk_UnIN n i'), rtac ctxt @{thm CollectI},
             REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, etac ctxt conjI, assume_tac ctxt,
             rtac ctxt trans, rtac ctxt @{thm shift_def}, rtac ctxt iffD2, rtac ctxt @{thm fun_eq_iff}, rtac ctxt allI,
             CONVERSION (Conv.top_conv
@@ -651,7 +651,7 @@
 
 fun mk_congruent_str_final_tac ctxt m lsbisE map_comp_id map_cong0 equiv_LSBISs =
   EVERY' [rtac ctxt @{thm congruentI}, dtac ctxt lsbisE,
-    REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, bexE], rtac ctxt (o_apply RS trans),
+    REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE bexE}, rtac ctxt (o_apply RS trans),
     etac ctxt (sym RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans),
     rtac ctxt (map_cong0 RS trans), REPEAT_DETERM_N m o rtac ctxt refl,
     EVERY' (map (fn equiv_LSBIS =>
@@ -663,7 +663,7 @@
   EVERY' [rtac ctxt (coalg_def RS iffD2),
     CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
       EVERY' [rtac ctxt @{thm univ_preserves}, rtac ctxt equiv_LSBIS, rtac ctxt congruent_str_final,
-        rtac ctxt ballI, rtac ctxt @{thm ssubst_mem}, rtac ctxt o_apply, rtac ctxt CollectI,
+        rtac ctxt @{thm ballI}, rtac ctxt @{thm ssubst_mem}, rtac ctxt o_apply, rtac ctxt @{thm CollectI},
         REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV],
         CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
           EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans),
@@ -675,22 +675,22 @@
 fun mk_mor_T_final_tac ctxt mor_def congruent_str_finals equiv_LSBISs =
   EVERY' [rtac ctxt (mor_def RS iffD2), rtac ctxt conjI,
     CONJ_WRAP' (fn equiv_LSBIS =>
-      EVERY' [rtac ctxt ballI, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff},
+      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff},
         rtac ctxt equiv_LSBIS, assume_tac ctxt])
     equiv_LSBISs,
     CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
-      EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm univ_commute}, rtac ctxt equiv_LSBIS,
+      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm univ_commute}, rtac ctxt equiv_LSBIS,
         rtac ctxt congruent_str_final, assume_tac ctxt, rtac ctxt o_apply])
     (equiv_LSBISs ~~ congruent_str_finals)] 1;
 
 fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
   unfold_thms_tac ctxt defs THEN
   EVERY' [rtac ctxt conjI,
-    CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps,
+    CONJ_WRAP' (fn thm => rtac ctxt @{thm ballI} THEN' rtac ctxt thm) Reps,
     CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) =>
-      EVERY' [rtac ctxt ballI, rtac ctxt (map_comp_id RS trans), rtac ctxt map_cong0L,
+      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (map_comp_id RS trans), rtac ctxt map_cong0L,
         EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
-          EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt Abs_inverse,
+          EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (o_apply RS trans), rtac ctxt Abs_inverse,
             etac ctxt set_rev_mp, rtac ctxt coalg_final_set, rtac ctxt Rep])
         Abs_inverses coalg_final_sets)])
     (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
@@ -698,8 +698,8 @@
 fun mk_mor_Abs_tac ctxt defs Abs_inverses =
   unfold_thms_tac ctxt defs THEN
   EVERY' [rtac ctxt conjI,
-    CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses,
-    CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' etac ctxt (thm RS arg_cong RS sym)) Abs_inverses] 1;
+    CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' rtac ctxt @{thm UNIV_I})) Abs_inverses,
+    CONJ_WRAP' (fn thm => rtac ctxt @{thm ballI} THEN' etac ctxt (thm RS arg_cong RS sym)) Abs_inverses] 1;
 
 fun mk_mor_unfold_tac ctxt m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
   EVERY' [rtac ctxt iffD2, rtac ctxt mor_UNIV,
@@ -727,12 +727,12 @@
       rtac ctxt mor_T_final, EVERY' (map (fn thm => rtac ctxt (thm RS @{thm relInvImage_Gr})) lsbis_incls),
       rtac ctxt impI,
       CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) =>
-        EVERY' [rtac ctxt subset_trans, rtac ctxt @{thm relInvImage_UNIV_relImage}, rtac ctxt subset_trans,
-          rtac ctxt @{thm relInvImage_mono}, rtac ctxt subset_trans, etac ctxt incl_lsbis,
+        EVERY' [rtac ctxt @{thm subset_trans}, rtac ctxt @{thm relInvImage_UNIV_relImage}, rtac ctxt @{thm subset_trans},
+          rtac ctxt @{thm relInvImage_mono}, rtac ctxt @{thm subset_trans}, etac ctxt incl_lsbis,
           rtac ctxt ord_eq_le_trans, rtac ctxt @{thm sym[OF relImage_relInvImage]},
           rtac ctxt @{thm xt1(3)}, rtac ctxt @{thm Sigma_cong},
           rtac ctxt @{thm proj_image}, rtac ctxt @{thm proj_image}, rtac ctxt lsbis_incl,
-          rtac ctxt subset_trans, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, assume_tac ctxt,
+          rtac ctxt @{thm subset_trans}, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, assume_tac ctxt,
           rtac ctxt @{thm relImage_proj}, rtac ctxt equiv_LSBIS, rtac ctxt @{thm relInvImage_Id_on},
           rtac ctxt Rep_inject])
       (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
@@ -742,13 +742,13 @@
   CONJ_WRAP' (fn (raw_coind, unfold_def) =>
     EVERY' [rtac ctxt @{thm ext}, etac ctxt (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac ctxt mor,
       rtac ctxt @{thm image2_eqI}, rtac ctxt refl, rtac ctxt (unfold_def RS arg_cong RS trans),
-      rtac ctxt (o_apply RS sym), rtac ctxt UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
+      rtac ctxt (o_apply RS sym), rtac ctxt @{thm UNIV_I}]) (raw_coinds ~~ unfold_defs) 1;
 
 fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors =
   unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply,
     rtac ctxt trans, rtac ctxt unfold, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L,
     EVERY' (map (fn thm =>
-      rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
+      rtac ctxt @{thm ballI} THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
     rtac ctxt sym, rtac ctxt id_apply] 1;
 
 fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
@@ -770,11 +770,11 @@
       REPEAT_DETERM o etac ctxt allE, rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
       REPEAT_DETERM_N m o rtac ctxt refl,
       REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_case_prod_eq[symmetric]},
-      etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm case_prodD}])
+      etac ctxt mp, etac ctxt @{thm CollectE}, etac ctxt @{thm case_prodD}])
     rel_congs,
     rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
     CONJ_WRAP' (K (EVERY' [rtac ctxt impI, rtac ctxt @{thm IdD}, etac ctxt set_mp,
-      rtac ctxt CollectI, etac ctxt @{thm case_prodI}])) rel_congs] 1;
+      rtac ctxt @{thm CollectI}, etac ctxt @{thm case_prodI}])) rel_congs] 1;
 
 fun mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0 =
   EVERY' [rtac ctxt @{thm ext}, rtac ctxt (o_apply RS trans RS sym), rtac ctxt (o_apply RS trans RS sym),
@@ -789,8 +789,8 @@
     REPEAT_DETERM_N n o rtac ctxt @{thm Un_upper1},
     REPEAT_DETERM_N n o
       EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets =>
-        EVERY' [rtac ctxt subsetI, rtac ctxt @{thm UnI2}, rtac ctxt (mk_UnIN n i), etac ctxt @{thm UN_I},
-          etac ctxt UnE, etac ctxt set_Jset, REPEAT_DETERM_N (n - 1) o etac ctxt UnE,
+        EVERY' [rtac ctxt @{thm subsetI}, rtac ctxt @{thm UnI2}, rtac ctxt (mk_UnIN n i), etac ctxt @{thm UN_I},
+          etac ctxt @{thm UnE}, etac ctxt set_Jset, REPEAT_DETERM_N (n - 1) o etac ctxt @{thm UnE},
           EVERY' (map (fn thm => EVERY' [etac ctxt @{thm UN_E}, etac ctxt thm, assume_tac ctxt]) set_Jset_Jsets)])
       (1 upto n) set_Jsets set_Jset_Jsetss)] 1;
 
@@ -831,27 +831,27 @@
          REPEAT_DETERM_N n o rtac ctxt fst_convol_fun_cong_sym,
          rtac ctxt map_comp_trans, rtac ctxt sym, rtac ctxt dtor_maps_trans, rtac ctxt map_cong0,
          EVERY' (maps (fn set_Jset =>
-           [rtac ctxt o_apply_trans_sym, rtac ctxt (@{thm snd_conv} RS trans), etac ctxt CollectE,
-           REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, etac ctxt set_Jset]) set_Jsets),
+           [rtac ctxt o_apply_trans_sym, rtac ctxt (@{thm snd_conv} RS trans), etac ctxt @{thm CollectE},
+           REPEAT_DETERM o etac ctxt conjE, etac ctxt @{thm bspec}, etac ctxt set_Jset]) set_Jsets),
          REPEAT_DETERM_N n o rtac ctxt snd_convol_fun_cong_sym,
-         rtac ctxt CollectI,
+         rtac ctxt @{thm CollectI},
          EVERY' (map (fn set_map0 => EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
-           rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, rtac ctxt refl])
+           rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm case_prodI}, rtac ctxt refl])
         (take m set_map0s)),
          CONJ_WRAP' (fn (set_map0, set_Jset_Jsets) =>
            EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
-             rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, rtac ctxt exI, rtac ctxt conjI,
-             rtac ctxt CollectI, etac ctxt CollectE,
+             rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm case_prodI}, rtac ctxt exI, rtac ctxt conjI,
+             rtac ctxt @{thm CollectI}, etac ctxt @{thm CollectE},
              REPEAT_DETERM o etac ctxt conjE,
              CONJ_WRAP' (fn set_Jset_Jset =>
-               EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_Jset_Jset, assume_tac ctxt]) set_Jset_Jsets,
+               EVERY' [rtac ctxt @{thm ballI}, etac ctxt @{thm bspec}, etac ctxt set_Jset_Jset, assume_tac ctxt]) set_Jset_Jsets,
              rtac ctxt (conjI OF [refl, refl])])
            (drop m set_map0s ~~ set_Jset_Jsetss)])
         (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
           map_cong0s ~~ set_map0ss ~~ set_Jsetss ~~ set_Jset_Jsetsss ~~ in_rels) @
       [rtac ctxt impI,
        CONJ_WRAP' (fn k =>
-         EVERY' [rtac ctxt impI, dtac ctxt (mk_conjunctN n k), etac ctxt mp, rtac ctxt exI, rtac ctxt conjI, etac ctxt CollectI,
+         EVERY' [rtac ctxt impI, dtac ctxt (mk_conjunctN n k), etac ctxt mp, rtac ctxt exI, rtac ctxt conjI, etac ctxt @{thm CollectI},
            rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl]) ks]) 1
   end
 
@@ -898,7 +898,7 @@
         REPEAT_DETERM_N (n - 1) o rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound_strict})),
         EVERY' (map2 (fn i => fn set_sbd => EVERY' [
           rtac ctxt (@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [sbd_regularCard,
-          sbd_Cinfinite]), rtac ctxt set_sbd, rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE,
+          sbd_Cinfinite]), rtac ctxt set_sbd, rtac ctxt @{thm ballI}, REPEAT_DETERM o etac ctxt allE,
           etac ctxt (mk_conjunctN n i)]) (1 upto n) (drop m set_sbds))])
       (rec_Sucs ~~ set_sbdss)] 1
   end;
@@ -906,7 +906,7 @@
 fun mk_set_bd_tac ctxt sbd_Cinfinite sbd_regularCard natLeq_ordLess_bd col_bd =
   EVERY' (map (rtac ctxt) [@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [
     sbd_regularCard, sbd_Cinfinite], @{thm ordIso_ordLess_trans}, @{thm card_of_nat},
-    natLeq_ordLess_bd, ballI, col_bd]) 1;
+    natLeq_ordLess_bd, @{thm ballI}, col_bd]) 1;
 
 fun mk_le_rel_OO_tac ctxt coinduct rel_Jrels le_rel_OOs =
   EVERY' (rtac ctxt coinduct :: map2 (fn rel_Jrel => fn le_rel_OO =>
@@ -920,21 +920,21 @@
 fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
   ALLGOALS (TRY o (eresolve_tac ctxt coind_wits THEN' rtac ctxt refl)) THEN
   REPEAT_DETERM (assume_tac ctxt 1 ORELSE
-    EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set,
+    EVERY' [dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, resolve_tac ctxt dtor_set,
     K (unfold_thms_tac ctxt dtor_ctors),
-    REPEAT_DETERM_N n o etac ctxt UnE,
+    REPEAT_DETERM_N n o etac ctxt @{thm UnE},
     REPEAT_DETERM o
-      (TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN'
+      (TRY o REPEAT_DETERM o etac ctxt @{thm UnE} THEN' TRY o etac ctxt @{thm UN_E} THEN'
         (eresolve_tac ctxt wit ORELSE'
         (dresolve_tac ctxt wit THEN'
           (etac ctxt FalseE ORELSE'
-          EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set,
-            K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac ctxt UnE]))))] 1);
+          EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, resolve_tac ctxt dtor_set,
+            K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac ctxt @{thm UnE}]))))] 1);
 
 fun mk_coind_wit_tac ctxt induct unfolds set_nats wits =
   rtac ctxt induct 1 THEN ALLGOALS (TRY o rtac ctxt impI THEN' TRY o hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
-  ALLGOALS (REPEAT_DETERM o etac ctxt imageE THEN' TRY o hyp_subst_tac ctxt) THEN
+  ALLGOALS (REPEAT_DETERM o etac ctxt @{thm imageE} THEN' TRY o hyp_subst_tac ctxt) THEN
   ALLGOALS (TRY o
     FIRST' [rtac ctxt TrueI, rtac ctxt refl, etac ctxt (refl RSN (2, mp)), dresolve_tac ctxt wits THEN' etac ctxt FalseE]);
 
@@ -963,16 +963,16 @@
     val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
     val in_Jrel = nth in_Jrels (i - 1);
     val if_tac =
-      EVERY' [dtac ctxt (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
-        rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+      EVERY' [dtac ctxt (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE},
+        rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
         EVERY' (map2 (fn set_map0 => fn set_incl =>
           EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
             rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply,
             etac ctxt (set_incl RS @{thm subset_trans})])
         passive_set_map0s dtor_set_incls),
         CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
-          EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
-            rtac ctxt @{thm case_prodI}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+          EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI},
+            rtac ctxt @{thm case_prodI}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
             CONJ_WRAP' (fn thm => etac ctxt (thm RS @{thm subset_trans}) THEN' assume_tac ctxt) dtor_set_set_incls,
             rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl])
         (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
@@ -983,8 +983,8 @@
           rtac ctxt trans, rtac ctxt sym, rtac ctxt dtor_map, rtac ctxt (dtor_inject RS iffD2), assume_tac ctxt])
         @{thms fst_conv snd_conv}];
     val only_if_tac =
-      EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
-        rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+      EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE},
+        rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
         CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
           EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt dtor_set, rtac ctxt @{thm Un_least},
             rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals}, rtac ctxt passive_set_map0,
@@ -993,14 +993,14 @@
               (fn (active_set_map0, in_Jrel) => EVERY' [rtac ctxt ord_eq_le_trans,
                 rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]},
                 rtac ctxt active_set_map0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt @{thm UN_least},
-                dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
+                dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt @{thm imageE},
                 dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
-                REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
-                  @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
+                REPEAT_DETERM o eresolve_tac ctxt
+                  @{thms CollectE conjE case_prodE iffD1[OF prod.inject, elim_format]},
                 hyp_subst_tac ctxt,
                 dtac ctxt (in_Jrel RS iffD1),
                 dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
-                REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
+                REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, assume_tac ctxt])
             (rev (active_set_map0s ~~ in_Jrels))])
         (dtor_sets ~~ passive_set_map0s),
         rtac ctxt conjI,
@@ -1009,8 +1009,8 @@
           rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
           EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt,
             dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
-            REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
-              @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
+            REPEAT_DETERM o eresolve_tac ctxt
+              @{thms CollectE conjE case_prodE iffD1[OF prod.inject, elim_format]},
             hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1),
             dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) in_Jrels),
           assume_tac ctxt]]
@@ -1031,7 +1031,7 @@
         EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2],
           REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
           select_prem_tac ctxt (length ks) (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
-          REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
+          REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, hyp_subst_tac ctxt,
           rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI), rtac ctxt conjI,
           rtac ctxt (map_comp0 RS trans), rtac ctxt (dtor_map RS trans RS sym),
           rtac ctxt (dtor_unfold RS map_arg_cong RS trans), rtac ctxt (trans OF [map_comp0, map_cong]),
@@ -1042,10 +1042,10 @@
           REPEAT_DETERM_N n o (rtac ctxt @{thm trans[OF o_apply]} THEN' rtac ctxt @{thm snd_conv}),
           etac ctxt (@{thm prod.case} RS map_arg_cong RS trans),
           SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case o_def fst_conv snd_conv}),
-          rtac ctxt CollectI,
+          rtac ctxt @{thm CollectI},
           CONJ_WRAP' (fn set_map0 =>
             EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans),
-              rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI},
+              rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI}, rtac ctxt @{thm case_prodI},
               FIRST' [rtac ctxt refl, EVERY'[rtac ctxt exI, rtac ctxt conjI, etac ctxt Collect_splitD_set_mp,
                 assume_tac ctxt, rtac ctxt (@{thm surjective_pairing} RS arg_cong)]]])
           set_map0s])
@@ -1061,18 +1061,18 @@
     EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
       EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
         select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
-        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
+        REPEAT_DETERM o eresolve_tac ctxt [@{thm CollectE}, @{thm conjE}, Collect_splitD_set_mp, set_rev_mp],
         hyp_subst_tac ctxt,
         SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
-        rtac ctxt subset_refl])
+        rtac ctxt @{thm subset_refl}])
     unfolds set_map0ss ks) 1 THEN
     EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
       EVERY' (map (fn set_map0 =>
         EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
         select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
-        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
+        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, hyp_subst_tac ctxt,
         SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),
-        etac ctxt imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp],
+        etac ctxt @{thm imageE}, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp],
         rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, assume_tac ctxt,
         rtac ctxt (@{thm surjective_pairing} RS arg_cong)])
       (drop m set_map0s)))
@@ -1087,13 +1087,13 @@
     REPEAT_DETERM (etac ctxt exE 1) THEN
     CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
       EVERY' [rtac ctxt @{thm predicate2I}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI,
-        if null helper_inds then rtac ctxt UNIV_I
-        else rtac ctxt CollectI THEN'
+        if null helper_inds then rtac ctxt @{thm UNIV_I}
+        else rtac ctxt @{thm CollectI} THEN'
           CONJ_WRAP' (fn helper_ind =>
             EVERY' [rtac ctxt (helper_ind RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
               REPEAT_DETERM_N n o etac ctxt thin_rl, rtac ctxt impI,
-              REPEAT_DETERM o resolve_tac ctxt [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
-              dtac ctxt bspec, assume_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
+              REPEAT_DETERM o resolve_tac ctxt @{thms subsetI CollectI iffD2[OF split_beta]},
+              dtac ctxt @{thm bspec}, assume_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
               etac ctxt (refl RSN (2, conjI))])
           helper_inds,
         rtac ctxt conjI,
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Sun May 18 14:33:01 2025 +0000
@@ -214,7 +214,7 @@
       end;
 
     val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
-    val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
+    val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m @{thm subset_refl})) bnfs;
     val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
 
     val timer = time (timer "Derived simple theorems");
@@ -461,7 +461,7 @@
           val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
             typedef (sbdT_bind, sum_bdT_params', NoSyn)
               (HOLogic.mk_UNIV sum_bdT) NONE (fn ctxt =>
-                EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+                EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
 
           val sbdT = Type (sbdT_name, sum_bdT_params);
           val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
@@ -751,12 +751,12 @@
 
     val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
       typedef (IIT_bind, params, NoSyn)
-        (HOLogic.mk_UNIV II_repT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+        (HOLogic.mk_UNIV II_repT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
 
     val IIT = Type (IIT_name, params');
     val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT);
     val Rep_IIT = Const (#Rep_name IIT_glob_info, IIT --> II_repT);
-    val Abs_IIT_inverse_thm = UNIV_I RS #Abs_inverse IIT_loc_info;
+    val Abs_IIT_inverse_thm = @{thm UNIV_I} RS #Abs_inverse IIT_loc_info;
 
     val initT = IIT --> Asuc_bdT;
     val active_initTs = replicate n initT;
@@ -1080,7 +1080,7 @@
       end;
 
     val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
-      ((rtac lthy CollectI THEN' CONJ_WRAP' (K (rtac lthy @{thm subset_UNIV})) (1 upto m + n)) 1)
+      ((rtac lthy @{thm CollectI} THEN' CONJ_WRAP' (K (rtac lthy @{thm subset_UNIV})) (1 upto m + n)) 1)
       (mor_fold_thm RS morE)) morE_thms;
 
     val (fold_unique_mor_thms, fold_unique_mor_thm) =
@@ -1389,7 +1389,7 @@
               val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) =
                 typedef (sbd0T_bind, sum_bd0T_params', NoSyn)
                   (HOLogic.mk_UNIV sum_bd0T) NONE (fn ctxt =>
-                    EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
+                    EVERY' [rtac ctxt exI, rtac ctxt @{thm UNIV_I}] 1) lthy;
 
               val sbd0T = Type (sbd0T_name, sum_bd0T_params);
               val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T);
@@ -1564,8 +1564,8 @@
 
         fun mk_set_thms ctor_set = (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper1}]) ::
           map (fn i => (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper2}]) RS
-            (mk_Un_upper n i RS subset_trans) RSN
-            (2, @{thm UN_upper} RS subset_trans))
+            (mk_Un_upper n i RS @{thm subset_trans}) RSN
+            (2, @{thm UN_upper} RS @{thm subset_trans}))
             (1 upto n);
         val set_Iset_thmsss = transpose (map (map mk_set_thms) ctor_Iset_thmss);
 
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sun May 18 14:33:01 2025 +0000
@@ -86,20 +86,20 @@
 val ord_eq_le_trans = @{thm ord_eq_le_trans};
 val subset_trans = @{thm subset_trans};
 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
-val rev_bspec = Drule.rotate_prems 1 bspec;
+val rev_bspec = Drule.rotate_prems 1 @{thm bspec};
 val Un_cong = @{thm arg_cong2[of _ _ _ _ "(\<union>)"]};
 val relChainD = @{thm iffD2[OF meta_eq_to_obj_eq[OF relChain_def]]};
 
 fun mk_alg_set_tac ctxt alg_def =
-  EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, rtac ctxt CollectI,
+  EVERY' [dtac ctxt (alg_def RS iffD1), REPEAT_DETERM o etac ctxt conjE, etac ctxt @{thm bspec}, rtac ctxt @{thm CollectI},
    REPEAT_DETERM o (rtac ctxt (subset_UNIV RS conjI) ORELSE' etac ctxt conjI), assume_tac ctxt] 1;
 
 fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
   (EVERY' [rtac ctxt notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN'
   REPEAT_DETERM o FIRST'
     [EVERY' [rtac ctxt @{thm subset_emptyI}, eresolve_tac ctxt wits],
-    EVERY' [rtac ctxt subsetI, rtac ctxt FalseE, eresolve_tac ctxt wits],
-    EVERY' [rtac ctxt subsetI, dresolve_tac ctxt wits, hyp_subst_tac ctxt,
+    EVERY' [rtac ctxt @{thm subsetI}, rtac ctxt FalseE, eresolve_tac ctxt wits],
+    EVERY' [rtac ctxt @{thm subsetI}, dresolve_tac ctxt wits, hyp_subst_tac ctxt,
       FIRST' (map (fn thm => rtac ctxt thm THEN' assume_tac ctxt) alg_sets)]] THEN'
   etac ctxt @{thm emptyE}) 1;
 
@@ -107,30 +107,30 @@
   (dtac ctxt (mor_def RS iffD1) THEN'
   REPEAT o etac ctxt conjE THEN'
   TRY o rtac ctxt @{thm image_subsetI} THEN'
-  etac ctxt bspec THEN'
+  etac ctxt @{thm bspec} THEN'
   assume_tac ctxt) 1;
 
 fun mk_mor_incl_tac ctxt mor_def map_ids =
   (rtac ctxt (mor_def RS iffD2) THEN'
   rtac ctxt conjI THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
+  CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
     map_ids THEN'
   CONJ_WRAP' (fn thm =>
-    (EVERY' [rtac ctxt ballI, rtac ctxt trans, rtac ctxt id_apply, stac ctxt thm, rtac ctxt refl])) map_ids) 1;
+    (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt trans, rtac ctxt id_apply, stac ctxt thm, rtac ctxt refl])) map_ids) 1;
 
 fun mk_mor_comp_tac ctxt mor_def set_maps map_comp_ids =
   let
     val fbetw_tac =
-      EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}),
-        etac ctxt bspec, etac ctxt bspec, assume_tac ctxt];
+      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (o_apply RS @{thm ssubst_mem}),
+        etac ctxt @{thm bspec}, etac ctxt @{thm bspec}, assume_tac ctxt];
     fun mor_tac (set_map, map_comp_id) =
-      EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans,
+      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt (o_apply RS trans), rtac ctxt trans,
         rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong,
-         REPEAT o eresolve_tac ctxt [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN'
+         REPEAT o eresolve_tac ctxt @{thms CollectE conjE}, etac ctxt @{thm bspec}, rtac ctxt @{thm CollectI}] THEN'
       CONJ_WRAP' (fn thm =>
         FIRST' [rtac ctxt subset_UNIV,
           (EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
-            etac ctxt bspec, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN'
+            etac ctxt @{thm bspec}, etac ctxt set_mp, assume_tac ctxt])]) set_map THEN'
       rtac ctxt (map_comp_id RS arg_cong);
   in
     (dtac ctxt (mor_def RS iffD1) THEN' dtac ctxt (mor_def RS iffD1) THEN' rtac ctxt (mor_def RS iffD2) THEN'
@@ -142,20 +142,20 @@
 
 fun mk_mor_str_tac ctxt ks mor_def =
   (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt UNIV_I])) ks THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, rtac ctxt refl])) ks) 1;
+  CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm UNIV_I}])) ks THEN'
+  CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, rtac ctxt refl])) ks) 1;
 
 fun mk_mor_UNIV_tac ctxt m morEs mor_def =
   let
     val n = length morEs;
     fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE,
-      rtac ctxt CollectI, CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto m + n),
+      rtac ctxt @{thm CollectI}, CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto m + n),
       rtac ctxt sym, rtac ctxt o_apply];
   in
     EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs,
-    rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs,
+    rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' rtac ctxt @{thm UNIV_I})) morEs,
     REPEAT_DETERM o etac ctxt conjE, REPEAT_DETERM_N n o dtac ctxt (@{thm fun_eq_iff} RS iffD1),
-    CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, rtac ctxt trans,
+    CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o etac ctxt allE, rtac ctxt trans,
       etac ctxt (o_apply RS sym RS trans), rtac ctxt o_apply])) morEs] 1
   end;
 
@@ -164,17 +164,17 @@
     val n = length alg_sets;
     fun set_tac thm =
       EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans, etac ctxt @{thm image_mono},
-        rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on}];
+        rtac ctxt @{thm equalityD1}, etac ctxt @{thm bij_betw_imp_surj_on}];
     val alg_tac =
       CONJ_WRAP' (fn (set_maps, alg_set) =>
-        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp,
-          rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imp_surj_on[OF bij_betw_the_inv_into]},
-          rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
+        EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt set_mp,
+          rtac ctxt @{thm equalityD1}, etac ctxt @{thm bij_betw_imp_surj_on[OF bij_betw_the_inv_into]},
+          rtac ctxt @{thm imageI}, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
       (set_mapss ~~ alg_sets);
 
     val mor_tac = rtac ctxt conjI THEN' CONJ_WRAP' (K (etac ctxt @{thm bij_betwE})) alg_sets THEN'
       CONJ_WRAP' (fn (set_maps, alg_set) =>
-        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
+        EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
           etac ctxt @{thm f_the_inv_into_f_bij_betw}, etac ctxt alg_set,
           EVERY' (map set_tac (drop m set_maps))])
       (set_mapss ~~ alg_sets);
@@ -187,15 +187,15 @@
   EVERY' [REPEAT_DETERM o etac ctxt conjE, rtac ctxt rev_mp, rtac ctxt @{thm Cinfinite_limit_finite},
     REPEAT_DETERM_N n o rtac ctxt @{thm finite.insertI}, rtac ctxt @{thm finite.emptyI},
     REPEAT_DETERM_N n o etac ctxt @{thm insert_subsetI}, rtac ctxt @{thm empty_subsetI},
-    rtac ctxt bd_Cinfinite, rtac ctxt impI, etac ctxt bexE, rtac ctxt bexI,
+    rtac ctxt bd_Cinfinite, rtac ctxt impI, etac ctxt @{thm bexE}, rtac ctxt @{thm bexI},
     CONJ_WRAP' (fn i =>
-      EVERY' [etac ctxt bspec, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}])
+      EVERY' [etac ctxt @{thm bspec}, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1}])
       (0 upto n - 1),
     assume_tac ctxt] 1;
 
 fun mk_min_algs_tac ctxt worel in_congs =
   let
-    val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt bspec,
+    val minG_tac = EVERY' [rtac ctxt @{thm SUP_cong}, rtac ctxt refl, dtac ctxt @{thm bspec},
       assume_tac ctxt, etac ctxt arg_cong];
     fun minH_tac thm =
       EVERY' [rtac ctxt Un_cong, minG_tac, rtac ctxt @{thm image_cong}, rtac ctxt thm,
@@ -208,9 +208,9 @@
   end;
 
 fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac ctxt relChainD, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
-  rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt subsetI,
-  rtac ctxt UnI1, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt,
-  assume_tac ctxt, rtac ctxt equalityD1, dtac ctxt @{thm notnotD},
+  rtac ctxt @{thm case_split}, rtac ctxt @{thm xt1(3)}, rtac ctxt min_algs, etac ctxt @{thm FieldI2}, rtac ctxt @{thm subsetI},
+  rtac ctxt @{thm UnI1}, rtac ctxt @{thm UN_I}, etac ctxt @{thm underS_I}, assume_tac ctxt,
+  assume_tac ctxt, rtac ctxt @{thm equalityD1}, dtac ctxt @{thm notnotD},
   hyp_subst_tac ctxt, rtac ctxt refl] 1;
 
 fun mk_min_algs_card_of_tac ctxt cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
@@ -234,7 +234,7 @@
 
     val minG_tac = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordLess_imp_ordLeq},
       rtac ctxt @{thm ordLess_transitive}, rtac ctxt @{thm card_of_underS}, rtac ctxt suc_Card_order,
-      assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt ballI, etac ctxt allE,
+      assume_tac ctxt, rtac ctxt suc_Asuc, rtac ctxt @{thm ballI}, etac ctxt allE,
       dtac ctxt mp, etac ctxt @{thm underS_E},
       dtac ctxt mp, etac ctxt @{thm underS_Field},
       REPEAT o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite]
@@ -271,7 +271,7 @@
 
     fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg,
       rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI},
-      REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], etac ctxt alg_set,
+      REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, etac ctxt alg_set,
       REPEAT_DETERM o (etac ctxt subset_trans THEN' minG_tac)];
   in
     (rtac ctxt induct THEN'
@@ -284,21 +284,21 @@
   let
     val n = length min_algs;
     fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY'
-      [rtac ctxt bexE, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono,
+      [rtac ctxt @{thm bexE}, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono,
        etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac ctxt set_bds];
     fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) =
-      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
-        EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE,
+      EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
+        EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt @{thm bexE},
         rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, assume_tac ctxt,
         rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}),
         rtac ctxt @{thm UN_I}, REPEAT_DETERM_N (m + 3 * n) o etac ctxt thin_rl,
         assume_tac ctxt, rtac ctxt set_mp,
-        rtac ctxt equalityD2, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt UnI2,
+        rtac ctxt @{thm equalityD2}, rtac ctxt min_alg, assume_tac ctxt, rtac ctxt @{thm UnI2},
         rtac ctxt @{thm image_eqI}, rtac ctxt refl,
-        rtac ctxt CollectI, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl,
+        rtac ctxt @{thm CollectI}, REPEAT_DETERM_N m o dtac ctxt asm_rl, REPEAT_DETERM_N n o etac ctxt thin_rl,
         REPEAT_DETERM o etac ctxt conjE,
         CONJ_WRAP' (K (FIRST' [assume_tac ctxt,
-          EVERY' [etac ctxt subset_trans, rtac ctxt subsetI, rtac ctxt @{thm UN_I},
+          EVERY' [etac ctxt subset_trans, rtac ctxt @{thm subsetI}, rtac ctxt @{thm UN_I},
             etac ctxt @{thm underS_I}, assume_tac ctxt, assume_tac ctxt]]))
           set_bds];
   in
@@ -310,7 +310,7 @@
   EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt (min_alg_def RS @{thm card_of_ordIso_subst}),
     rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt @{thm ordIso_ordLeq_trans},
     rtac ctxt @{thm card_of_Field_ordIso}, rtac ctxt suc_Card_order, rtac ctxt @{thm ordLess_imp_ordLeq},
-    rtac ctxt suc_Asuc, rtac ctxt ballI, dtac ctxt rev_mp, rtac ctxt card_of,
+    rtac ctxt suc_Asuc, rtac ctxt @{thm ballI}, dtac ctxt rev_mp, rtac ctxt card_of,
     REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt, rtac ctxt Asuc_Cinfinite] 1;
 
 fun mk_least_min_alg_tac ctxt min_alg_def least =
@@ -319,8 +319,8 @@
     REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt] 1;
 
 fun mk_alg_select_tac ctxt Abs_inverse =
-  EVERY' [rtac ctxt ballI,
-    REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
+  EVERY' [rtac ctxt @{thm ballI},
+    REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE}, hyp_subst_tac ctxt] 1 THEN
   unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN assume_tac ctxt 1;
 
 fun mk_mor_select_tac ctxt mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets
@@ -329,16 +329,16 @@
     val n = length alg_sets;
     val fbetw_tac =
       CONJ_WRAP'
-        (K (EVERY' [rtac ctxt ballI, etac ctxt rev_bspec,
-          etac ctxt CollectE, assume_tac ctxt])) alg_sets;
+        (K (EVERY' [rtac ctxt @{thm ballI}, etac ctxt rev_bspec,
+          etac ctxt @{thm CollectE}, assume_tac ctxt])) alg_sets;
     val mor_tac =
-      CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
+      CONJ_WRAP' (fn thm => EVERY' [rtac ctxt @{thm ballI}, rtac ctxt thm]) str_init_defs;
     fun alg_epi_tac ((alg_set, str_init_def), set_map) =
-      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
-        rtac ctxt ballI, forward_tac ctxt [alg_select RS bspec],
+      EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt @{thm CollectI},
+        rtac ctxt @{thm ballI}, forward_tac ctxt [alg_select RS @{thm bspec}],
         rtac ctxt (str_init_def RS @{thm ssubst_mem}),
         etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map,
-          rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
+          rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt @{thm bspec},
           assume_tac ctxt]];
   in
     EVERY' [rtac ctxt mor_cong, REPEAT_DETERM_N n o (rtac ctxt sym THEN' rtac ctxt @{thm comp_id}),
@@ -355,7 +355,7 @@
       REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp,
       rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt,
       rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
-      rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI,
+      rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt @{thm CollectI}, REPEAT_DETERM o rtac ctxt exI,
       rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
       SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
       etac ctxt mor_comp, rtac ctxt mor_incl, REPEAT_DETERM_N n o rtac ctxt subset_UNIV] 1
@@ -368,7 +368,7 @@
     val ks = (1 upto n);
 
     fun mor_tac morE in_mono = EVERY' [etac ctxt morE, rtac ctxt set_mp, rtac ctxt in_mono,
-      REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI,
+      REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt @{thm CollectI},
       REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)];
     fun cong_tac ct map_cong0 = EVERY'
       [rtac ctxt (map_cong0 RS infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong),
@@ -376,8 +376,8 @@
       REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)];
 
     fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) =
-      EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
-        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
+      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm CollectI},
+        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
         REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
         rtac ctxt trans, mor_tac morE in_mono,
         rtac ctxt trans, cong_tac ct map_cong0,
@@ -395,17 +395,17 @@
   let
     val n = length least_min_algs;
 
-    fun mk_alg_tac alg_set = EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
-      REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
+    fun mk_alg_tac alg_set = EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm CollectI},
+      REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
       REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
-      rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI,
+      rtac ctxt mp, etac ctxt @{thm bspec}, rtac ctxt @{thm CollectI},
       REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
       CONJ_WRAP' (K (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict})) alg_sets,
-      CONJ_WRAP' (K (rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt))
+      CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt))
         alg_sets];
 
     fun mk_induct_tac least_min_alg =
-      rtac ctxt ballI THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN'
+      rtac ctxt @{thm ballI} THEN' etac ctxt @{thm prop_restrict} THEN' rtac ctxt least_min_alg THEN'
       rtac ctxt (alg_def RS iffD2) THEN'
       CONJ_WRAP' mk_alg_tac alg_sets;
   in
@@ -415,9 +415,9 @@
 fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses alg_min_alg alg_sets set_mapss =
   unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
   EVERY' [rtac ctxt conjI,
-    CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps,
+    CONJ_WRAP' (fn thm => rtac ctxt @{thm ballI} THEN' rtac ctxt thm) Reps,
     CONJ_WRAP' (fn (Abs_inverse, (set_maps, alg_set)) =>
-      EVERY' [rtac ctxt ballI, rtac ctxt Abs_inverse, rtac ctxt (alg_min_alg RS alg_set),
+      EVERY' [rtac ctxt @{thm ballI}, rtac ctxt Abs_inverse, rtac ctxt (alg_min_alg RS alg_set),
         EVERY' (map2 (fn Rep => fn set_map =>
           EVERY' [rtac ctxt (set_map RS ord_eq_le_trans), rtac ctxt @{thm image_subsetI}, rtac ctxt Rep])
         Reps (drop m set_maps))])
@@ -426,12 +426,12 @@
 fun mk_mor_Abs_tac ctxt cts defs Abs_inverses map_comp_ids map_congLs =
   unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
   EVERY' [rtac ctxt conjI,
-    CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses,
+    CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' rtac ctxt @{thm UNIV_I})) Abs_inverses,
     CONJ_WRAP' (fn (ct, thm) =>
-      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
+      EVERY' [rtac ctxt @{thm ballI}, REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
         rtac ctxt (thm RS (infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong) RS sym),
         EVERY' (map (fn Abs_inverse =>
-          EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
+          EVERY' [rtac ctxt (o_apply RS trans RS @{thm ballI}), etac ctxt (set_mp RS Abs_inverse),
             assume_tac ctxt])
         Abs_inverses)])
     (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;
@@ -445,7 +445,7 @@
   let
     fun mk_unique type_def =
       EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}),
-        rtac ctxt ballI, resolve_tac ctxt init_unique_mors,
+        rtac ctxt @{thm ballI}, resolve_tac ctxt init_unique_mors,
         EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps),
         rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt,
         rtac ctxt mor_comp, rtac ctxt mor_Abs, rtac ctxt mor_fold];
@@ -456,7 +456,7 @@
 fun mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
   EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt (dtor_def RS fun_cong RS trans),
     rtac ctxt trans, rtac ctxt foldx, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L,
-    EVERY' (map (fn thm => rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply]))
+    EVERY' (map (fn thm => rtac ctxt @{thm ballI} THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply]))
       ctor_o_folds),
     rtac ctxt sym, rtac ctxt id_apply] 1;
 
@@ -477,19 +477,19 @@
     val ks = 1 upto n;
 
     fun mk_IH_tac Rep_inv Abs_inv set_map =
-      DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt bspec,
-        dtac ctxt set_rev_mp, rtac ctxt equalityD1, rtac ctxt set_map, etac ctxt imageE,
+      DETERM o EVERY' [dtac ctxt meta_mp, rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt @{thm bspec},
+        dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, rtac ctxt set_map, etac ctxt @{thm imageE},
         hyp_subst_tac ctxt, rtac ctxt (Abs_inv RS @{thm ssubst_mem}), etac ctxt set_mp,
         assume_tac ctxt, assume_tac ctxt];
 
     fun mk_closed_tac (k, (morE, set_maps)) =
-      EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt ballI, rtac ctxt impI,
+      EVERY' [select_prem_tac ctxt n (dtac ctxt asm_rl) k, rtac ctxt @{thm ballI}, rtac ctxt impI,
         rtac ctxt (mor_Abs RS morE RS arg_cong RS iffD2), assume_tac ctxt,
-        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], dtac ctxt @{thm meta_spec},
+        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, dtac ctxt @{thm meta_spec},
         EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), assume_tac ctxt];
 
     fun mk_induct_tac (Rep, Rep_inv) =
-      EVERY' [rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt (Rep RSN (2, bspec))];
+      EVERY' [rtac ctxt (Rep_inv RS arg_cong RS iffD1), etac ctxt (Rep RSN (2, @{thm bspec}))];
   in
     (rtac ctxt mp THEN' rtac ctxt impI THEN'
     DETERM o CONJ_WRAP_GEN' (etac ctxt conjE THEN' rtac ctxt conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'
@@ -572,7 +572,7 @@
       rtac ctxt (@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [
         bd_regularCard, bd_Cinfinite, set_bd
       ]),
-      rtac ctxt ballI,
+      rtac ctxt @{thm ballI},
       Goal.assume_rule_tac ctxt
     ];
 
@@ -587,11 +587,11 @@
 
 fun mk_mcong_tac ctxt induct_tac set_setsss map_cong0s ctor_maps =
   let
-    fun use_asm thm = EVERY' [etac ctxt bspec, etac ctxt set_rev_mp, rtac ctxt thm];
+    fun use_asm thm = EVERY' [etac ctxt @{thm bspec}, etac ctxt set_rev_mp, rtac ctxt thm];
 
     fun useIH set_sets = EVERY' [rtac ctxt mp, Goal.assume_rule_tac ctxt,
       CONJ_WRAP' (fn thm =>
-        EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_rev_mp, etac ctxt thm]) set_sets];
+        EVERY' [rtac ctxt @{thm ballI}, etac ctxt @{thm bspec}, etac ctxt set_rev_mp, etac ctxt thm]) set_sets];
 
     fun mk_map_cong0 ctor_map map_cong0 set_setss =
       EVERY' [rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
@@ -610,9 +610,9 @@
       REPEAT_DETERM_N 2 o dtac ctxt (Irel RS iffD1), rtac ctxt (Irel RS iffD2),
       rtac ctxt rel_mono, rtac ctxt (le_rel_OO RS @{thm predicate2D}),
       rtac ctxt @{thm relcomppI}, assume_tac ctxt, assume_tac ctxt,
-      REPEAT_DETERM_N m o EVERY' [rtac ctxt ballI, rtac ctxt ballI, rtac ctxt impI, assume_tac ctxt],
+      REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm ballI}, rtac ctxt impI, assume_tac ctxt],
       REPEAT_DETERM_N (length le_rel_OOs) o
-        EVERY' [rtac ctxt ballI, rtac ctxt ballI, Goal.assume_rule_tac ctxt]])
+        EVERY' [rtac ctxt @{thm ballI}, rtac ctxt @{thm ballI}, Goal.assume_rule_tac ctxt]])
   ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1;
 
 (* BNF tactics *)
@@ -645,14 +645,14 @@
 
 fun mk_wit_tac ctxt n ctor_set wit =
   REPEAT_DETERM (assume_tac ctxt 1 ORELSE
-    EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set,
+    EVERY' [dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, resolve_tac ctxt ctor_set,
     REPEAT_DETERM o
-      (TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN'
+      (TRY o REPEAT_DETERM o etac ctxt @{thm UnE} THEN' TRY o etac ctxt @{thm UN_E} THEN'
         (eresolve_tac ctxt wit ORELSE'
         (dresolve_tac ctxt wit THEN'
           (etac ctxt FalseE ORELSE'
-          EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt ctor_set,
-            REPEAT_DETERM_N n o etac ctxt UnE]))))] 1);
+          EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt @{thm equalityD1}, resolve_tac ctxt ctor_set,
+            REPEAT_DETERM_N n o etac ctxt @{thm UnE}]))))] 1);
 
 fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject
   ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss =
@@ -665,16 +665,16 @@
     val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
     val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
     val if_tac =
-      EVERY' [dtac ctxt (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
-        rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+      EVERY' [dtac ctxt (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE},
+        rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
         EVERY' (map2 (fn set_map0 => fn ctor_set_incl =>
           EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
             rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply,
             rtac ctxt (ctor_set_incl RS subset_trans), etac ctxt le_arg_cong_ctor_dtor])
         passive_set_map0s ctor_set_incls),
         CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) =>
-          EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
-            rtac ctxt @{thm case_prodI}, rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+          EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm CollectI},
+            rtac ctxt @{thm case_prodI}, rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
             CONJ_WRAP' (fn thm =>
               EVERY' (map (etac ctxt) [thm RS subset_trans, le_arg_cong_ctor_dtor]))
             ctor_set_set_incls,
@@ -688,8 +688,8 @@
           etac ctxt eq_arg_cong_ctor_dtor])
         fst_snd_convs];
     val only_if_tac =
-      EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
-        rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
+      EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE},
+        rtac ctxt (in_Irel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt @{thm CollectI},
         CONJ_WRAP' (fn (ctor_set, passive_set_map0) =>
           EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt ctor_set, rtac ctxt @{thm Un_least},
             rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals[OF _ refl]},
@@ -697,13 +697,13 @@
             CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
               (fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans,
                 rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least},
-                dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
+                dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt @{thm imageE},
                 dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
-                REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
-                  @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
+                REPEAT_DETERM o eresolve_tac ctxt
+                  @{thms CollectE conjE case_prodE iffD1[OF prod.inject, elim_format]},
                 hyp_subst_tac ctxt,
                 dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
-                REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
+                REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, assume_tac ctxt])
             (rev (active_set_map0s ~~ in_Irels))])
         (ctor_sets ~~ passive_set_map0s),
         rtac ctxt conjI,
@@ -713,8 +713,8 @@
           EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply,
             dtac ctxt set_rev_mp, assume_tac ctxt,
             dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
-            REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
-              @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
+            REPEAT_DETERM o eresolve_tac ctxt
+              @{thms CollectE conjE case_prodE iffD1[OF prod.inject, elim_format]},
             hyp_subst_tac ctxt,
             dtac ctxt (in_Irel RS iffD1), dtac ctxt @{thm someI_ex},
             REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Sun May 18 14:33:01 2025 +0000
@@ -623,14 +623,14 @@
 
             fun rel_OO_Grp_tac ctxt =
               HEADGOAL (EVERY' ([SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt ext))),
-                SELECT_GOAL (unfold_thms_tac ctxt [@{thm OO_Grp_alt}, mem_Collect_eq,
-                  o_apply, @{thm vimage2p_def}, in_rel_of_bnf bnf_F, Bex_def, mem_Collect_eq]),
+                SELECT_GOAL (unfold_thms_tac ctxt (@{thms OO_Grp_alt mem_Collect_eq
+                  o_apply vimage2p_def} @ in_rel_of_bnf bnf_F :: @{thms Bex_def mem_Collect_eq})),
                 rtac ctxt iffI,
                 SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [exE, conjE]))),
                 forward_tac ctxt
                   [zip_closed_thm OF (replicate 2 (Rep_thm RSN (2, @{thm ssubst_mem})))],
                 assume_tac ctxt,
-                SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [bexE, conjE]))),
+                SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt @{thms bexE conjE}))),
                 etac ctxt Rep_cases_thm,
                 hyp_subst_tac ctxt,
                 SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt exI))),
@@ -813,11 +813,11 @@
           REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
           REPEAT_DETERM o dtac ctxt (mk_sym set_F'_rsp),
           SELECT_GOAL (unfold_thms_tac ctxt [#set_map_F' set_F'_thms]),
-          rtac ctxt ballI, dtac ctxt @{thm equalityD1[THEN subsetD]}, assume_tac ctxt,
+          rtac ctxt @{thm ballI}, dtac ctxt @{thm equalityD1[THEN subsetD]}, assume_tac ctxt,
           SELECT_GOAL (unfold_thms_tac ctxt @{thms image_iff}),
-          etac ctxt bexE, dtac ctxt set_mp, assume_tac ctxt,
+          etac ctxt @{thm bexE}, dtac ctxt set_mp, assume_tac ctxt,
           SELECT_GOAL (unfold_thms_tac ctxt @{thms mem_Collect_eq case_prod_beta}),
-          rtac ctxt bexI, hyp_subst_tac ctxt, assume_tac ctxt, etac ctxt @{thm hypsubst},
+          rtac ctxt @{thm bexI}, hyp_subst_tac ctxt, assume_tac ctxt, etac ctxt @{thm hypsubst},
           etac ctxt @{thm imageI}, assume_tac ctxt]
       end;
   in
@@ -1132,10 +1132,10 @@
                 replicate live @{thm Grp_conversep_nonempty} RS rev_mp),
               rtac ctxt impI, dtac ctxt @{thm predicate2D}, etac ctxt @{thm relcomppI2[rotated]},
               rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]},
-              REPEAT_DETERM o resolve_tac ctxt [CollectI, conjI, subset_UNIV],
+              REPEAT_DETERM o resolve_tac ctxt @{thms CollectI conjI subset_UNIV},
               rtac ctxt (rel_flip RS iffD2),
               rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]},
-              REPEAT_DETERM o resolve_tac ctxt [CollectI, conjI, subset_UNIV],
+              REPEAT_DETERM o resolve_tac ctxt @{thms CollectI conjI subset_UNIV},
               SELECT_GOAL (unfold_thms_tac ctxt (rel_eq_onp :: @{thms Grp_conversep_eq_onp})),
               etac ctxt @{thm predicate2D[OF rel_conj_eq_onp, rotated]},
               rtac ctxt equiv_thm']);
@@ -1204,21 +1204,21 @@
               fun F_in'_mono_tac ctxt =
                 unfold_thms_tac ctxt [#def F_in', #def F_in] THEN
                 HEADGOAL (EVERY'
-                  [rtac ctxt subsetI,
-                  etac ctxt vimageE,
+                  [rtac ctxt @{thm subsetI},
+                  etac ctxt @{thm vimageE},
                   etac ctxt @{thm ImageE},
-                  etac ctxt CollectE,
-                  etac ctxt CollectE,
+                  etac ctxt @{thm CollectE},
+                  etac ctxt @{thm CollectE},
                   dtac ctxt @{thm case_prodD},
                   hyp_subst_tac ctxt,
-                  rtac ctxt (vimageI OF [refl]),
+                  rtac ctxt @{thm vimageI [OF refl]},
                   rtac ctxt @{thm ImageI},
-                  rtac ctxt CollectI,
+                  rtac ctxt @{thm CollectI},
                   rtac ctxt @{thm case_prodI},
                   assume_tac ctxt ORELSE' rtac ctxt refl,
-                  rtac ctxt CollectI,
-                  etac ctxt subset_trans,
-                  etac ctxt (@{thm insert_mono} OF [@{thm image_mono}])]);
+                  rtac ctxt @{thm CollectI},
+                  etac ctxt @{thm subset_trans},
+                  etac ctxt @{thm insert_mono [OF image_mono]}]);
               val F_in'_mono_thm = prove lthy [var_A, var_A'] F_in'_mono_tm F_in'_mono_tac;
 
               (* F_in'_Inter: F_in' (\<Inter>S) = (\<Inter>A\<in>S. F_in' A) *)
@@ -1234,13 +1234,13 @@
                       (unfold_thms_tac ctxt @{thms Inter_empty INT_empty UNIV_sum_unit_conv}),
                     rtac ctxt @{thm set_eqI},
                     rtac ctxt iffI,
-                    rtac ctxt UNIV_I,
-                    rtac ctxt (vimageI OF [refl]),
+                    rtac ctxt @{thm UNIV_I},
+                    rtac ctxt @{thm vimageI [OF refl]},
                     rtac ctxt @{thm ImageI},
-                    rtac ctxt CollectI,
+                    rtac ctxt @{thm CollectI},
                     rtac ctxt @{thm case_prodI},
                     rtac ctxt (#reflp qthms),
-                    rtac ctxt CollectI,
+                    rtac ctxt @{thm CollectI},
                     rtac ctxt subset_UNIV,
                     etac ctxt @{thm exE[OF ex_in_conv[THEN iffD2]]},
                     EqSubst.eqsubst_tac ctxt [0] @{thms image_INT[of _ UNIV _ id, simplified]},
@@ -1248,31 +1248,31 @@
                     assume_tac ctxt,
                     SELECT_GOAL (unfold_thms_tac ctxt @{thms INT_extend_simps vimage_INT[symmetric]}),
                     rtac ctxt @{thm arg_cong2[where f=vimage, OF refl]},
-                    rtac ctxt equalityI,
-                    rtac ctxt subsetI,
+                    rtac ctxt @{thm equalityI},
+                    rtac ctxt @{thm subsetI},
                     rtac ctxt @{thm InterI},
-                    etac ctxt imageE,
+                    etac ctxt @{thm imageE},
                     etac ctxt @{thm ImageE},
-                    etac ctxt CollectE,
-                    etac ctxt CollectE,
+                    etac ctxt @{thm CollectE},
+                    etac ctxt @{thm CollectE},
                     dtac ctxt @{thm case_prodD},
                     hyp_subst_tac ctxt,
                     rtac ctxt @{thm ImageI[OF CollectI]},
                     etac ctxt @{thm case_prodI} ORELSE' (SELECT_GOAL
                       (unfold_thms_tac ctxt @{thms prod.case}) THEN' rtac ctxt @{thm refl}),
-                    rtac ctxt CollectI,
-                    etac ctxt subset_trans,
+                    rtac ctxt @{thm CollectI},
+                    etac ctxt @{thm subset_trans},
                     etac ctxt @{thm INT_lower[OF imageI]},
                     rtac ctxt (@{thm subset_trans} OF [asm_rl, rel_Inter_thm]),
                     K (unfold_thms_tac ctxt @{thms image_image}),
-                    rtac ctxt subset_refl,
+                    rtac ctxt @{thm subset_refl},
                     K (unfold_thms_tac ctxt @{thms INT_extend_simps ex_in_conv[symmetric]}),
                     rtac ctxt exI,
-                    rtac ctxt imageI,
+                    rtac ctxt @{thm imageI},
                     assume_tac ctxt,
                     rtac ctxt exI,
                     rtac ctxt @{thm InterI},
-                    etac ctxt imageE,
+                    etac ctxt @{thm imageE},
                     hyp_subst_tac ctxt,
                     rtac ctxt @{thm insertI1}]);
 
@@ -1298,22 +1298,22 @@
               (* F_in'_alt2: F_in' A = {x. set_F' x \<subseteq> A} *)
               val F_in'_alt2_tm = mk_Trueprop_eq
                 (#tm F_in' $ var_A, mk_in [var_A] [#tm set_F'] typ_aF);
-              fun F_in'_alt2_tac ctxt = HEADGOAL (rtac ctxt equalityI THEN'
+              fun F_in'_alt2_tac ctxt = HEADGOAL (rtac ctxt @{thm equalityI} THEN'
                 (Subgoal.FOCUS o K) (unfold_thms_tac ctxt (map #def [set_F', F_in', F_in])) ctxt
                 THEN' EVERY'
-                  [rtac ctxt subsetI,
-                  rtac ctxt CollectI,
-                  rtac ctxt subsetI,
-                  dtac ctxt vimageD,
+                  [rtac ctxt @{thm subsetI},
+                  rtac ctxt @{thm CollectI},
+                  rtac ctxt @{thm subsetI},
+                  dtac ctxt @{thm vimageD},
                   etac ctxt @{thm ImageE},
-                  etac ctxt CollectE,
-                  etac ctxt CollectE,
+                  etac ctxt @{thm CollectE},
+                  etac ctxt @{thm CollectE},
                   dtac ctxt @{thm case_prodD},
                   dtac ctxt @{thm InterD},
                   rtac ctxt @{thm imageI[OF CollectI]},
                   etac ctxt (#symp qthms),
                   etac ctxt @{thm UnionE},
-                  etac ctxt imageE,
+                  etac ctxt @{thm imageE},
                   hyp_subst_tac ctxt,
                   etac ctxt @{thm subset_lift_sum_unitD},
                   etac ctxt @{thm setr.cases},
@@ -1321,28 +1321,28 @@
                   assume_tac ctxt])
                 THEN unfold_thms_tac ctxt [#def set_F'] THEN
                 (HEADGOAL o EVERY')
-                  [rtac ctxt subsetI,
-                  etac ctxt CollectE,
-                  etac ctxt (subsetD OF [F_in'_mono_thm]),
+                  [rtac ctxt @{thm subsetI},
+                  etac ctxt @{thm CollectE},
+                  etac ctxt (@{thm subsetD} OF [F_in'_mono_thm]),
                   EqSubst.eqsubst_tac ctxt [0] [F_in'_Inter_thm],
                   rtac ctxt @{thm InterI}] THEN
                 REPEAT_DETERM (HEADGOAL (etac ctxt @{thm imageE} THEN' hyp_subst_tac ctxt)) THEN
                 (HEADGOAL o EVERY')
-                  [etac ctxt CollectE,
+                  [etac ctxt @{thm CollectE},
                   SELECT_GOAL (unfold_thms_tac ctxt (map #def [F_in', F_in])),
                   rtac ctxt @{thm vimageI[OF refl]},
                   rtac ctxt @{thm ImageI},
-                  rtac ctxt CollectI,
+                  rtac ctxt @{thm CollectI},
                   rtac ctxt @{thm case_prodI},
                   etac ctxt (#symp qthms),
-                  rtac ctxt CollectI,
-                  rtac ctxt subsetI,
+                  rtac ctxt @{thm CollectI},
+                  rtac ctxt @{thm subsetI},
                   rtac ctxt @{thm sum_insert_Inl_unit},
                   assume_tac ctxt,
                   hyp_subst_tac ctxt,
-                  rtac ctxt imageI,
+                  rtac ctxt @{thm imageI},
                   rtac ctxt @{thm UnionI},
-                  rtac ctxt imageI,
+                  rtac ctxt @{thm imageI},
                   assume_tac ctxt,
                   rtac ctxt @{thm setr.intros[OF refl]}];
               val F_in'_alt2_thm = prove lthy [var_A] F_in'_alt2_tm F_in'_alt2_tac;
@@ -1355,22 +1355,22 @@
                   [rtac ctxt @{thm set_eqI},
                   rtac ctxt iffI,
                   rtac ctxt @{thm InterI},
-                  etac ctxt CollectE,
-                  etac ctxt CollectE,
-                  dtac ctxt subsetD,
+                  etac ctxt @{thm CollectE},
+                  etac ctxt @{thm CollectE},
+                  dtac ctxt @{thm subsetD},
                   assume_tac ctxt,
                   assume_tac ctxt,
                   etac ctxt @{thm InterD},
-                  rtac ctxt CollectI,
-                  rtac ctxt CollectI,
-                  rtac ctxt subset_refl]);
+                  rtac ctxt @{thm CollectI},
+                  rtac ctxt @{thm CollectI},
+                  rtac ctxt @{thm subset_refl}]);
               val set_F'_alt_thm = prove lthy [var_x] set_F'_alt_tm set_F'_alt_tac;
 
               (* map_F_in_F_in'I: x \<in> F_in' B \<Longrightarrow> map_F f x \<in> F_in' (f ` B) *)
               val map_F_in_F_in'I_tm = mk_Trueprop_implies ([HOLogic.mk_mem (var_x, #tm F_in' $ var_A')],
                 HOLogic.mk_mem (map_F_fs_x, subst_b (#tm F_in') $ (mk_image var_f $ var_A')));
               fun map_F_in_F_in'I_tac ctxt =
-                Local_Defs.unfold_tac ctxt ([#def F_in', #def F_in, Bex_def] @ @{thms vimage_def Image_iff}) THEN
+                Local_Defs.unfold_tac ctxt (#def F_in' :: #def F_in :: @{thms Bex_def vimage_def Image_iff}) THEN
                 HEADGOAL (EVERY'
                   [etac ctxt @{thm CollectE},
                   etac ctxt exE,
@@ -1386,7 +1386,7 @@
                   dtac ctxt (map_F_rsp_of (map mk_Maybe_map var_fs) ctxt),
                   SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: @{thms o_def map_sum.simps})),
                   assume_tac ctxt,
-                  rtac ctxt CollectI,
+                  rtac ctxt @{thm CollectI},
                   SELECT_GOAL (unfold_thms_tac ctxt set_map_thms),
                   etac ctxt @{thm image_map_sum_unit_subset}]);
               val map_F_in_F_in'I_thm =
@@ -1422,7 +1422,7 @@
                   fun subset_UNIVs n = fold (fn a => fn b => conjI OF [a, b]) (replicate (n-1)
                     @{thm subset_UNIV}) @{thm subset_UNIV};
                   val GrpI_inst = infer_instantiate' ctxt (map SOME [Thm.cterm_of ctxt map_F_fs, x])
-                    @{thm GrpI} OF [refl, CollectI] OF [subset_UNIVs live];
+                    @{thm GrpI} OF @{thms refl CollectI} OF [subset_UNIVs live];
 
                 in EVERY [
                   HEADGOAL (Method.insert_tac ctxt [rel_pos_distr_thm_inst]),
@@ -1437,7 +1437,7 @@
                     rtac ctxt @{thm relcomppI},
                     rtac ctxt rel_refl_strong]),
                   REPEAT_DETERM_N idx (HEADGOAL (rtac ctxt refl)),
-                  HEADGOAL (rtac ctxt conjI THEN' TWICE (etac ctxt subsetD THEN' assume_tac ctxt)),
+                  HEADGOAL (rtac ctxt conjI THEN' TWICE (etac ctxt @{thm subsetD} THEN' assume_tac ctxt)),
                   REPEAT_DETERM_N (live-idx-1) (HEADGOAL (rtac ctxt refl)),
                   HEADGOAL (EVERY'
                     [rtac ctxt @{thm relcomppI},
@@ -1453,24 +1453,24 @@
                     etac ctxt @{thm GrpE},
                     hyp_subst_tac ctxt,
                     rtac ctxt @{thm ImageI},
-                    rtac ctxt CollectI,
+                    rtac ctxt @{thm CollectI},
                     rtac ctxt @{thm case_prodI},
                     assume_tac ctxt,
                     EqSubst.eqsubst_asm_tac ctxt [1] rel_map,
                     EqSubst.eqsubst_asm_tac ctxt [1] [in_rel_of_bnf bnf_F],
                     etac ctxt exE,
-                    etac ctxt CollectE,
+                    etac ctxt @{thm CollectE},
                     etac ctxt conjE,
                     etac ctxt conjE,
-                    etac ctxt CollectE,
+                    etac ctxt @{thm CollectE},
                     hyp_subst_tac ctxt,
-                    rtac ctxt CollectI]),
+                    rtac ctxt @{thm CollectI}]),
                   unfold_thms_tac ctxt set_map_thms,
-                  HEADGOAL (rtac ctxt (subsetI OF [vimageI] OF [refl]) THEN'
+                  HEADGOAL (rtac ctxt (@{thm subsetI} OF @{thms vimageI} OF [refl]) THEN'
                             etac ctxt @{thm imageE} THEN' hyp_subst_tac ctxt),
                   REPEAT_DETERM_N 6 (HEADGOAL (etac ctxt Drule.thin_rl)),
                   REPEAT_DETERM_N (live-1) (HEADGOAL (etac ctxt conjE)),
-                  HEADGOAL (EVERY' [dtac ctxt subsetD, assume_tac ctxt, etac ctxt CollectE]),
+                  HEADGOAL (EVERY' [dtac ctxt @{thm subsetD}, assume_tac ctxt, etac ctxt @{thm CollectE}]),
                   unfold_thms_tac ctxt @{thms split_beta},
                   HEADGOAL (etac ctxt conjunct2)] end;
 
@@ -1478,20 +1478,20 @@
                 [rtac ctxt @{thm set_eqI},
                 rtac ctxt iffI,
                 etac ctxt @{thm ImageE},
-                etac ctxt CollectE,
-                etac ctxt CollectE,
+                etac ctxt @{thm CollectE},
+                etac ctxt @{thm CollectE},
                 dtac ctxt @{thm case_prodD},
-                rtac ctxt (vimageI OF [refl]),
+                rtac ctxt @{thm vimageI [OF refl]},
                 rtac ctxt @{thm ImageI},
-                rtac ctxt CollectI,
+                rtac ctxt @{thm CollectI},
                 rtac ctxt @{thm case_prodI},
                 etac ctxt map_F_rsp,
-                rtac ctxt CollectI,
+                rtac ctxt @{thm CollectI},
                 EqSubst.eqsubst_tac ctxt [0] [set_map_F_thm],
                 etac ctxt @{thm subset_vimage_image_subset},
-                etac ctxt vimageE,
+                etac ctxt @{thm vimageE},
                 etac ctxt @{thm ImageE},
-                TWICE (etac ctxt CollectE),
+                TWICE (etac ctxt @{thm CollectE}),
                 dtac ctxt @{thm case_prodD},
                 hyp_subst_tac ctxt,
                 Subgoal.FOCUS_PARAMS subgoal_tac ctxt]);
@@ -1506,18 +1506,18 @@
                   rtac ctxt iffI,
                   EqSubst.eqsubst_asm_tac ctxt [0] [set_F'_alt_thm],
                   etac ctxt @{thm InterD},
-                  rtac ctxt CollectI,
+                  rtac ctxt @{thm CollectI},
                   rtac ctxt map_F_in_F_in'I_thm,
                   SELECT_GOAL (unfold_thms_tac ctxt [F_in'_alt2_thm]),
-                  rtac ctxt CollectI,
-                  rtac ctxt subset_refl,
+                  rtac ctxt @{thm CollectI},
+                  rtac ctxt @{thm subset_refl},
                   SELECT_GOAL (unfold_thms_tac ctxt [set_F'_alt_thm]),
                   rtac ctxt @{thm InterI},
-                  etac ctxt imageE,
-                  etac ctxt CollectE,
+                  etac ctxt @{thm imageE},
+                  etac ctxt @{thm CollectE},
                   hyp_subst_tac ctxt,
                   etac ctxt @{thm vimageD[OF InterD]},
-                  rtac ctxt CollectI]) THEN
+                  rtac ctxt @{thm CollectI}]) THEN
                   (* map_F f x \<in> F_in' X \<Longrightarrow> x \<in> F_in' (f -` X) *)
                   HEADGOAL (Subgoal.FOCUS_PARAMS (fn {context = ctxt, params, ...} =>
                     let
@@ -1534,7 +1534,7 @@
                           @{thms lift_sum_unit_vimage_commute vimage_comp o_def map_sum.simps}),
                       unfold_thms_tac ctxt [@{thm o_def[symmetric]}, map_F_comp0],
                       Local_Defs.fold_tac ctxt @{thms vimage_comp},
-                      HEADGOAL (etac ctxt (vimageI OF [refl]))] end) ctxt);
+                      HEADGOAL (etac ctxt @{thm vimageI [OF refl]})] end) ctxt);
 
               (* set_F'_subset: set_F' x \<subseteq> set_F x *)
               val set_F'_subset_tm = HOLogic.mk_Trueprop (mk_leq (#tm set_F' $ var_x) (set_F $ var_x));
@@ -1542,17 +1542,17 @@
                 let val int_e_thm = infer_instantiate' ctxt
                   (replicate 3 NONE @ [SOME (Thm.cterm_of ctxt (map_F_Just $ var_x))]) @{thm INT_E};
                 in HEADGOAL (EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [#def set_F']),
-                  rtac ctxt subsetI,
+                  rtac ctxt @{thm subsetI},
                   etac ctxt int_e_thm,
                   SELECT_GOAL (unfold_thms_tac ctxt [set_map_F_thm]),
                   etac ctxt @{thm UN_E},
-                  etac ctxt imageE,
+                  etac ctxt @{thm imageE},
                   hyp_subst_tac ctxt,
                   SELECT_GOAL (unfold_thms_tac ctxt @{thms sum_set_simps singleton_iff}),
                   hyp_subst_tac ctxt,
                   assume_tac ctxt,
                   etac ctxt notE,
-                  rtac ctxt CollectI,
+                  rtac ctxt @{thm CollectI},
                   rtac ctxt (#reflp qthms)])
                 end;
             in
@@ -1594,9 +1594,9 @@
                 (unfold_thms_tac ctxt
                   (maps (fn {F_in'_def, F_in_def, ...} => [F_in'_def, F_in_def]) set_F'_thmss) ::
                 map (REPEAT_DETERM_N live o HEADGOAL)
-                  [etac ctxt vimageE,
+                  [etac ctxt @{thm vimageE},
                   etac ctxt @{thm ImageE},
-                  etac ctxt CollectE THEN' etac ctxt CollectE,
+                  etac ctxt @{thm CollectE} THEN' etac ctxt @{thm CollectE},
                   dtac ctxt @{thm case_prodD}] @
                 HEADGOAL (hyp_subst_tac ctxt THEN' rotate_tac (~live)) ::
                 map (fn i => (HEADGOAL o EVERY')
@@ -1610,7 +1610,7 @@
                   SELECT_GOAL (unfold_thms_tac ctxt (map_F_comp :: @{thms case_sum_o_inj(2)})),
                   EqSubst.eqsubst_tac ctxt [0] [map_F_cong OF replicate i refl @ asm_rl :: replicate (live-i) refl],
                   rtac ctxt @{thm sum.case_cong[OF refl refl]},
-                  etac ctxt bspec,
+                  etac ctxt @{thm bspec},
                   hyp_subst_tac ctxt,
                   etac ctxt @{thm subset_lift_sum_unitD},
                   assume_tac ctxt,
@@ -1641,9 +1641,9 @@
                   EVERY (map (fn {F_in'_alt2, ...} =>
                     unfold_thms_tac ctxt [F_in'_alt2] THEN
                     HEADGOAL (EVERY'
-                      [rtac ctxt CollectI,
-                      rtac ctxt subset_refl,
-                      rtac ctxt ballI,
+                      [rtac ctxt @{thm CollectI},
+                      rtac ctxt @{thm subset_refl},
+                      rtac ctxt @{thm ballI},
                       SELECT_GOAL (unfold_thms_tac ctxt [o_apply]),
                       rtac ctxt @{thm arg_cong[where f=Inr]},
                       asm_full_simp_tac ctxt])) set_F'_thmss) end;
@@ -1750,7 +1750,7 @@
                 [dtac ctxt (in_rel RS iffD1),
                 etac ctxt exE,
                 TWICE (etac ctxt conjE),
-                etac ctxt CollectE,
+                etac ctxt @{thm CollectE},
                 hyp_subst_tac ctxt]),
               (REPEAT_DETERM_N (live-1) o HEADGOAL) (etac ctxt conjE),
               HEADGOAL (Subgoal.FOCUS_PARAMS subgoal1_tac ctxt THEN' etac ctxt exE),
@@ -1834,7 +1834,7 @@
               REPEAT_FIRST (resolve_tac ctxt [conjI]),
               HEADGOAL (EVERY' (maps (fn {set_F'_respect, ...} =>
                 [etac ctxt @{thm subset_trans[rotated]},
-                rtac ctxt equalityD1,
+                rtac ctxt @{thm equalityD1},
                 rtac ctxt (@{thm rel_funD} OF [set_F'_respect]),
                 rtac ctxt (#rep_abs qthms),
                 rtac ctxt (#reflp qthms)]) set_F'_thmss)),
@@ -1927,9 +1927,9 @@
                 HEADGOAL (rtac ctxt exI),
                 HEADGOAL (EVERY' (maps (fn thms =>
                   [rtac ctxt conjI,
-                  rtac ctxt subsetI,
+                  rtac ctxt @{thm subsetI},
                   dtac ctxt (set_mp OF [#set_F'_subset thms]),
-                  dtac ctxt subsetD,
+                  dtac ctxt @{thm subsetD},
                   assume_tac ctxt, assume_tac ctxt]) set_F'_thmss)),
                 (REPEAT_DETERM o HEADGOAL)
                   (rtac ctxt conjI ORELSE' hyp_subst_tac ctxt THEN' rtac ctxt (#reflp qthms))]
@@ -2059,7 +2059,7 @@
   prepare_solve (K I) (K I) (K I) (K I) (K tacs) args;
 
 fun copy_bnf_tac {context = ctxt, prems = _} =
-  REPEAT_DETERM (resolve_tac ctxt [bexI, conjI, UNIV_I, refl, subset_refl] 1);
+  REPEAT_DETERM (resolve_tac ctxt @{thms bexI conjI UNIV_I refl subset_refl} 1);
 
 val copy_bnf =
   apfst (apfst (rpair NONE))
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun May 18 14:33:01 2025 +0000
@@ -569,7 +569,7 @@
 
         fun non_empty_typedef_tac non_empty_pred ctxt i =
           (Method.insert_tac ctxt [non_empty_pred] THEN' 
-            SELECT_GOAL (Local_Defs.unfold0_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i
+            SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms mem_Collect_eq}) THEN' assume_tac ctxt) i
         val uTname = unique_Tname (rty, qty)
         val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
         val ((_, tcode_dt), lthy2) = lthy1
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sun May 18 14:33:01 2025 +0000
@@ -105,14 +105,11 @@
 
 val unity_coeff_ex = Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] [] @{thm "unity_coeff_ex"};
 
-val [zdvd_mono,simp_from_to,all_not_ex] =
-     [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
-
 val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"};
 
 val eval_ss =
   simpset_of (put_simpset presburger_ss \<^context>
-    addsimps [simp_from_to] delsimps [insert_iff, bex_triv]);
+    addsimps @{thms simp_from_to} delsimps @{thms insert_iff bex_triv});
 fun eval_conv ctxt = Simplifier.rewrite (put_simpset eval_ss ctxt);
 
 (* recognising cterm without moving to terms *)
@@ -408,7 +405,7 @@
        val k = l div dest_number c
        val kt = HOLogic.mk_number iT k
        val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
-             ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
+             ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS @{thm zdvd_mono})
        val (d',t') = (mulC$kt$d, mulC$kt$r)
        val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop))
                    RS eq_reflection
@@ -571,7 +568,7 @@
 val conv_ss =
   simpset_of (put_simpset HOL_basic_ss \<^context>
     addsimps (@{thms simp_thms} @ take 4 @{thms ex_simps} @
-      [not_all, all_not_ex, @{thm ex_disj_distrib}]));
+      [not_all, @{thm all_not_ex}, @{thm ex_disj_distrib}]));
 
 fun conv ctxt p =
   Qelim.gen_qelim_conv ctxt
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Sun May 18 14:33:01 2025 +0000
@@ -153,10 +153,10 @@
   in
     EVERY' [rtac ctxt ext, SELECT_GOAL (Local_Defs.unfold0_tac ctxt [@{thm Domainp.simps},
         in_rel_of_bnf bnf, pred_def]), rtac ctxt iffI,
-        REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt,
-        CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt ballI, dtac ctxt (set_map RS equalityD1 RS set_mp),
-          etac ctxt imageE, dtac ctxt set_rev_mp, assume_tac ctxt,
-          REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm case_prodE}],
+        REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE}, hyp_subst_tac ctxt,
+        CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt @{thm ballI}, dtac ctxt (set_map RS @{thm equalityD1} RS set_mp),
+          etac ctxt @{thm imageE}, dtac ctxt set_rev_mp, assume_tac ctxt,
+          REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE case_prodE},
           hyp_subst_tac ctxt, rtac ctxt @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
           etac ctxt @{thm DomainPI}]) set_map's,
         REPEAT_DETERM o etac ctxt conjE,
@@ -164,10 +164,10 @@
         rtac ctxt refl, rtac ctxt (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym,
           map_id_of_bnf bnf]),
         REPEAT_DETERM_N n o (EVERY' [rtac ctxt @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]},
-          rtac ctxt @{thm fst_conv}]), rtac ctxt CollectI,
+          rtac ctxt @{thm fst_conv}]), rtac ctxt @{thm CollectI},
         CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt (set_map RS @{thm ord_eq_le_trans}),
-          REPEAT_DETERM o resolve_tac ctxt [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
-          dtac ctxt (rotate_prems 1 bspec), assume_tac ctxt,
+          REPEAT_DETERM o resolve_tac ctxt @{thms image_subsetI CollectI case_prodI},
+          dtac ctxt (rotate_prems 1 @{thm bspec}), assume_tac ctxt,
           etac ctxt @{thm DomainpE}, etac ctxt @{thm someI}]) set_map's
       ]
   end
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/record.ML	Sun May 18 14:33:01 2025 +0000
@@ -86,7 +86,7 @@
     (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =
   let
     val exists_thm =
-      UNIV_I
+      @{thm UNIV_I}
       |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
     val proj_constr = Abs_inverse OF [exists_thm];
     val absT = Type (tyco, map TFree vs);
@@ -103,7 +103,7 @@
     thy
     |> Named_Target.theory_map_result (apsnd o Typedef.transform_info)
         (Typedef.add_typedef overloaded (raw_tyco, vs, NoSyn)
-          (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1))
+          (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' @{thms UNIV_witness} 1))
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;
 
diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun May 18 14:33:01 2025 +0000
@@ -306,9 +306,9 @@
 (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
 fun list_of_Int th =
     (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
-    handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
+    handle THM _ => (list_of_Int (th RS @{thm IntD1}) @ list_of_Int (th RS @{thm IntD2}))
     handle THM _ => (list_of_Int (th RS @{thm INT_D}))
-    handle THM _ => (list_of_Int (th RS bspec))
+    handle THM _ => (list_of_Int (th RS @{thm bspec}))
     handle THM _ => [th];
 \<close>
 
@@ -319,7 +319,7 @@
   fun normalized th =
     normalized (th RS spec
       handle THM _ => th RS @{thm lessThanBspec}
-      handle THM _ => th RS bspec
+      handle THM _ => th RS @{thm bspec}
       handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
     handle THM _ => th;
 in