# HG changeset patch
# User blanchet
# Date 1347408305 -7200
# Node ID 8241f21d104bbc6222f36dbb70e0123cf888959f
# Parent  6964373dd6ac7d0e67c9fad1082eb020406ec3f4
tuned antiquotations

diff -r 6964373dd6ac -r 8241f21d104b src/HOL/Codatatype/Tools/bnf_comp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Wed Sep 12 02:05:04 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Wed Sep 12 02:05:05 2012 +0200
@@ -44,9 +44,19 @@
 open BNF_Util
 open BNF_Tactics
 
+val Card_order_csum = @{thm Card_order_csum};
+val Card_order_ctwo = @{thm Card_order_ctwo};
+val Cnotzero_UNIV = @{thm Cnotzero_UNIV};
 val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
+val card_of_Card_order = @{thm card_of_Card_order};
+val csum_Cnotzero1 = @{thm csum_Cnotzero1};
+val csum_Cnotzero2 = @{thm csum_Cnotzero2};
+val ctwo_Cnotzero = @{thm ctwo_Cnotzero};
 val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
+val ordIso_transitive = @{thm ordIso_transitive};
+val ordLeq_csum2 = @{thm ordLeq_csum2};
 val set_mp = @{thm set_mp};
+val subset_UNIV = @{thm subset_UNIV};
 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
 val trans_o_apply = @{thm trans[OF o_apply]};
 
@@ -80,7 +90,7 @@
      rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
      [REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac @{thm trans[OF image_insert]},
         rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
-        rtac @{thm trans[OF image_cong[OF o_apply refl]]}, rtac @{thm trans[OF image_image]},
+        rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]},
         rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
      rtac @{thm image_empty}]) 1;
 
@@ -152,9 +162,9 @@
     Local_Defs.unfold_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
     (REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
      REPEAT_DETERM (CHANGED ((
-       (rtac conjI THEN' (atac ORELSE' rtac @{thm subset_UNIV})) ORELSE'
+       (rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE'
        atac ORELSE'
-       (rtac @{thm subset_UNIV})) 1)) ORELSE rtac @{thm subset_UNIV} 1));
+       (rtac subset_UNIV)) 1)) ORELSE rtac subset_UNIV 1));
 
 fun mk_comp_in_bd_tac comp_in_alt Fin_bds Gin_bd Fbd_Cinfs Gbd_Card_order =
   let
@@ -166,9 +176,9 @@
         rtac bd_Cinf THEN'
         (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac next_bd_Cinf ORELSE'
            rtac next_bd_Cinf) THEN'
-        ((rtac @{thm Card_order_csum} THEN' rtac @{thm ordLeq_csum2}) ORELSE'
-          (rtac @{thm Card_order_ctwo} THEN' rtac @{thm ordLeq_refl})) THEN'
-        rtac @{thm Card_order_ctwo});
+        ((rtac Card_order_csum THEN' rtac ordLeq_csum2) ORELSE'
+          (rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl})) THEN'
+        rtac Card_order_ctwo);
   in
     (rtac @{thm ordIso_ordLeq_trans} THEN'
      rtac @{thm card_of_ordIso_subst} THEN'
@@ -182,23 +192,23 @@
      WRAP' gen_before gen_after (bds ~~ (Cinfs ~~ tl Fbd_Cinfs)) (rtac last_bd) THEN'
      rtac @{thm csum_absorb1} THEN'
      rtac @{thm Cinfinite_cexp} THEN'
-     (rtac @{thm ordLeq_csum2} ORELSE' rtac @{thm ordLeq_refl}) THEN'
-     rtac @{thm Card_order_ctwo} THEN'
+     (rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN'
+     rtac Card_order_ctwo THEN'
      (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE'
        rtac (hd Fbd_Cinfs)) THEN'
      rtac @{thm ctwo_ordLeq_Cinfinite} THEN'
      rtac @{thm Cinfinite_cexp} THEN'
-     (rtac @{thm ordLeq_csum2} ORELSE' rtac @{thm ordLeq_refl}) THEN'
-     rtac @{thm Card_order_ctwo} THEN'
+     (rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN'
+     rtac Card_order_ctwo THEN'
      (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE'
        rtac (hd Fbd_Cinfs)) THEN'
      rtac disjI1 THEN'
-     TRY o rtac @{thm csum_Cnotzero2} THEN'
-     rtac @{thm ctwo_Cnotzero} THEN'
+     TRY o rtac csum_Cnotzero2 THEN'
+     rtac ctwo_Cnotzero THEN'
      rtac Gbd_Card_order THEN'
      rtac @{thm cexp_cprod} THEN'
-     TRY o rtac @{thm csum_Cnotzero2} THEN'
-     rtac @{thm ctwo_Cnotzero}) 1
+     TRY o rtac csum_Cnotzero2 THEN'
+     rtac ctwo_Cnotzero) 1
   end;
 
 val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
@@ -234,28 +244,28 @@
 
 fun mk_kill_bd_cinfinite_tac bd_Cinfinite =
   (rtac @{thm cinfinite_cprod2} THEN'
-  TRY o rtac @{thm csum_Cnotzero1} THEN'
-  rtac @{thm Cnotzero_UNIV} THEN'
+  TRY o rtac csum_Cnotzero1 THEN'
+  rtac Cnotzero_UNIV THEN'
   rtac bd_Cinfinite) 1;
 
 fun mk_kill_set_bd_tac bd_Card_order set_bd =
   (rtac ctrans THEN'
   rtac set_bd THEN'
   rtac @{thm ordLeq_cprod2} THEN'
-  TRY o rtac @{thm csum_Cnotzero1} THEN'
-  rtac @{thm Cnotzero_UNIV} THEN'
+  TRY o rtac csum_Cnotzero1 THEN'
+  rtac Cnotzero_UNIV THEN'
   rtac bd_Card_order) 1
 
 val kill_in_alt_tac =
-  ((rtac @{thm Collect_cong} THEN' rtac @{thm iffI}) 1 THEN
+  ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN
   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
   REPEAT_DETERM (CHANGED ((etac conjI ORELSE'
-    rtac conjI THEN' rtac @{thm subset_UNIV}) 1)) THEN
-  (rtac @{thm subset_UNIV} ORELSE' atac) 1 THEN
+    rtac conjI THEN' rtac subset_UNIV) 1)) THEN
+  (rtac subset_UNIV ORELSE' atac) 1 THEN
   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
   REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1))) ORELSE
   ((rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN
-    REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm subset_UNIV} 1));
+    REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1));
 
 fun mk_kill_in_bd_tac n nontrivial_kill_in in_alt in_bd bd_Card_order bd_Cinfinite bd_Cnotzero =
   (rtac @{thm ordIso_ordLeq_trans} THEN'
@@ -266,65 +276,65 @@
   rtac @{thm ordIso_ordLeq_trans} THEN'
   rtac @{thm cexp_cong1}) 1 THEN
   (if nontrivial_kill_in then
-    rtac @{thm ordIso_transitive} 1 THEN
+    rtac ordIso_transitive 1 THEN
     REPEAT_DETERM_N (n - 1)
       ((rtac @{thm csum_cong1} THEN'
       rtac @{thm ordIso_symmetric} THEN'
       rtac @{thm csum_assoc} THEN'
-      rtac @{thm ordIso_transitive}) 1) THEN
+      rtac ordIso_transitive) 1) THEN
     (rtac @{thm ordIso_refl} THEN'
-    rtac @{thm Card_order_csum} THEN'
-    rtac @{thm ordIso_transitive} THEN'
+    rtac Card_order_csum THEN'
+    rtac ordIso_transitive THEN'
     rtac @{thm csum_assoc} THEN'
-    rtac @{thm ordIso_transitive} THEN'
+    rtac ordIso_transitive THEN'
     rtac @{thm csum_cong1} THEN'
     K (mk_flatten_assoc_tac
       (rtac @{thm ordIso_refl} THEN'
-        FIRST' [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}])
-      @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_cong}) THEN'
+        FIRST' [rtac card_of_Card_order, rtac Card_order_csum])
+      ordIso_transitive @{thm csum_assoc} @{thm csum_cong}) THEN'
     rtac @{thm ordIso_refl} THEN'
-    (rtac @{thm card_of_Card_order} ORELSE' rtac @{thm Card_order_csum})) 1
+    (rtac card_of_Card_order ORELSE' rtac Card_order_csum)) 1
   else all_tac) THEN
   (rtac @{thm csum_com} THEN'
   rtac bd_Card_order THEN'
   rtac disjI1 THEN'
-  rtac @{thm csum_Cnotzero2} THEN'
-  rtac @{thm ctwo_Cnotzero} THEN'
+  rtac csum_Cnotzero2 THEN'
+  rtac ctwo_Cnotzero THEN'
   rtac disjI1 THEN'
-  rtac @{thm csum_Cnotzero2} THEN'
-  TRY o rtac @{thm csum_Cnotzero1} THEN'
-  rtac @{thm Cnotzero_UNIV} THEN'
+  rtac csum_Cnotzero2 THEN'
+  TRY o rtac csum_Cnotzero1 THEN'
+  rtac Cnotzero_UNIV THEN'
   rtac @{thm ordLeq_ordIso_trans} THEN'
   rtac @{thm cexp_mono1} THEN'
   rtac ctrans THEN'
   rtac @{thm csum_mono2} THEN'
   rtac @{thm ordLeq_cprod1} THEN'
-  (rtac @{thm card_of_Card_order} ORELSE' rtac @{thm Card_order_csum}) THEN'
+  (rtac card_of_Card_order ORELSE' rtac Card_order_csum) THEN'
   rtac bd_Cnotzero THEN'
   rtac @{thm csum_cexp'} THEN'
   rtac @{thm Cinfinite_cprod2} THEN'
-  TRY o rtac @{thm csum_Cnotzero1} THEN'
-  rtac @{thm Cnotzero_UNIV} THEN'
+  TRY o rtac csum_Cnotzero1 THEN'
+  rtac Cnotzero_UNIV THEN'
   rtac bd_Cinfinite THEN'
-  ((rtac @{thm Card_order_ctwo} THEN' rtac @{thm ordLeq_refl}) ORELSE'
-    (rtac @{thm Card_order_csum} THEN' rtac @{thm ordLeq_csum2})) THEN'
-  rtac @{thm Card_order_ctwo} THEN'
+  ((rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl}) ORELSE'
+    (rtac Card_order_csum THEN' rtac ordLeq_csum2)) THEN'
+  rtac Card_order_ctwo THEN'
   rtac disjI1 THEN'
-  rtac @{thm csum_Cnotzero2} THEN'
-  TRY o rtac @{thm csum_Cnotzero1} THEN'
-  rtac @{thm Cnotzero_UNIV} THEN'
+  rtac csum_Cnotzero2 THEN'
+  TRY o rtac csum_Cnotzero1 THEN'
+  rtac Cnotzero_UNIV THEN'
   rtac bd_Card_order THEN'
   rtac @{thm cexp_cprod_ordLeq} THEN'
-  TRY o rtac @{thm csum_Cnotzero2} THEN'
-  rtac @{thm ctwo_Cnotzero} THEN'
+  TRY o rtac csum_Cnotzero2 THEN'
+  rtac ctwo_Cnotzero THEN'
   rtac @{thm Cinfinite_cprod2} THEN'
-  TRY o rtac @{thm csum_Cnotzero1} THEN'
-  rtac @{thm Cnotzero_UNIV} THEN'
+  TRY o rtac csum_Cnotzero1 THEN'
+  rtac Cnotzero_UNIV THEN'
   rtac bd_Cinfinite THEN'
   rtac bd_Cnotzero THEN'
   rtac @{thm ordLeq_cprod2} THEN'
-  TRY o rtac @{thm csum_Cnotzero1} THEN'
-  rtac @{thm Cnotzero_UNIV} THEN'
+  TRY o rtac csum_Cnotzero1 THEN'
+  rtac Cnotzero_UNIV THEN'
   rtac bd_Card_order) 1;
 
 
@@ -336,7 +346,7 @@
 fun mk_lift_set_bd_tac bd_Card_order = (rtac @{thm Card_order_empty} THEN' rtac bd_Card_order) 1;
 
 val lift_in_alt_tac =
-  ((rtac @{thm Collect_cong} THEN' rtac @{thm iffI}) 1 THEN
+  ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN
   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
   REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1)) THEN
   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
@@ -356,12 +366,12 @@
   ((rtac @{thm csum_mono1} 1 THEN
   REPEAT_DETERM_N (n - 1)
     ((rtac ctrans THEN'
-    rtac @{thm ordLeq_csum2} THEN'
-    (rtac @{thm Card_order_csum} ORELSE' rtac @{thm card_of_Card_order})) 1) THEN
-  (rtac @{thm ordLeq_csum2} THEN'
-  (rtac @{thm Card_order_csum} ORELSE' rtac @{thm card_of_Card_order})) 1) ORELSE
-  (rtac @{thm ordLeq_csum2} THEN' rtac @{thm Card_order_ctwo}) 1) THEN
-  (rtac disjI1 THEN' TRY o rtac @{thm csum_Cnotzero2} THEN' rtac @{thm ctwo_Cnotzero}
+    rtac ordLeq_csum2 THEN'
+    (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) THEN
+  (rtac ordLeq_csum2 THEN'
+  (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) ORELSE
+  (rtac ordLeq_csum2 THEN' rtac Card_order_ctwo) 1) THEN
+  (rtac disjI1 THEN' TRY o rtac csum_Cnotzero2 THEN' rtac ctwo_Cnotzero
    THEN' rtac bd_Card_order) 1;
 
 
@@ -383,16 +393,16 @@
   rtac @{thm csum_cong1} THEN'
   mk_rotate_eq_tac
     (rtac @{thm ordIso_refl} THEN'
-      FIRST' [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}])
-    @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
+      FIRST' [rtac card_of_Card_order, rtac Card_order_csum])
+    ordIso_transitive @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
     src dest THEN'
   rtac bd_Card_order THEN'
   rtac disjI1 THEN'
-  TRY o rtac @{thm csum_Cnotzero2} THEN'
-  rtac @{thm ctwo_Cnotzero} THEN'
+  TRY o rtac csum_Cnotzero2 THEN'
+  rtac ctwo_Cnotzero THEN'
   rtac disjI1 THEN'
-  TRY o rtac @{thm csum_Cnotzero2} THEN'
-  rtac @{thm ctwo_Cnotzero}) 1;
+  TRY o rtac csum_Cnotzero2 THEN'
+  rtac ctwo_Cnotzero) 1;
 
 fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
   (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN
diff -r 6964373dd6ac -r 8241f21d104b src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Wed Sep 12 02:05:04 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Wed Sep 12 02:05:05 2012 +0200
@@ -129,8 +129,24 @@
 open BNF_FP_Util
 open BNF_GFP_Util
 
+val Pair_eq_subst_id = @{thm Pair_eq[THEN subst, of "%x. x"]};
+val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;
+val list_inject_subst_id = @{thm list.inject[THEN subst, of "%x. x"]};
+val nat_induct = @{thm nat_induct};
+val o_apply_trans_sym = o_apply RS trans RS sym;
+val ord_eq_le_trans = @{thm ord_eq_le_trans};
+val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
+  @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
+val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
+val set_mp = @{thm set_mp};
+val set_rev_mp = @{thm set_rev_mp};
+val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
+val ssubst_id = @{thm ssubst[of _ _ "%x. x"]};
+val subst_id = @{thm subst[of _ _ "%x. x"]};
+val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
+
 fun mk_coalg_set_tac coalg_def =
-  dtac (coalg_def RS @{thm subst[of _ _ "\<lambda>x. x"]}) 1 THEN
+  dtac (coalg_def RS subst_id) 1 THEN
   REPEAT_DETERM (etac conjE 1) THEN
   EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN
   REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
@@ -145,7 +161,7 @@
 fun mk_mor_incl_tac mor_def map_id's =
   (stac mor_def THEN'
   rtac conjI THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ballI, etac @{thm set_mp}, stac @{thm id_apply}, atac]))
+  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac @{thm id_apply}, atac]))
     map_id's THEN'
   CONJ_WRAP' (fn thm =>
    (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (@{thm id_apply} RS arg_cong)]))
@@ -188,8 +204,8 @@
 
 fun mk_set_hset_incl_hset_tac n defs rec_Suc i =
   EVERY' (map (TRY oo stac) defs @
-    map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, @{thm set_mp}, equalityD2, rec_Suc,
-      UnI2, mk_UnN n i] @
+    map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2,
+      mk_UnN n i] @
     [etac @{thm UN_I}, atac]) 1;
 
 fun mk_set_incl_hin_tac incls =
@@ -198,13 +214,13 @@
     CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1;
 
 fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} =
-  EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+  EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
     REPEAT_DETERM o rtac allI,
     CONJ_WRAP' (fn thm => EVERY'
-      [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
+      [rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
     REPEAT_DETERM o rtac allI,
     CONJ_WRAP' (fn rec_Suc => EVERY'
-      [rtac @{thm ord_eq_le_trans}, rtac rec_Suc,
+      [rtac ord_eq_le_trans, rtac rec_Suc,
         if m = 0 then K all_tac
         else (rtac @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
         CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
@@ -213,13 +229,13 @@
       rec_Sucs] 1;
 
 fun mk_hset_minimal_tac n hset_defs hset_rec_minimal {context = ctxt, prems = _} =
-  (CONJ_WRAP' (fn def => (EVERY' [rtac @{thm ord_eq_le_trans}, rtac def,
+  (CONJ_WRAP' (fn def => (EVERY' [rtac ord_eq_le_trans, rtac def,
     rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal,
     EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
     REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1
 
 fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_naturalss coalg_setss =
-  EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+  EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
     REPEAT_DETERM o rtac allI,
     CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,
     REPEAT_DETERM o rtac allI,
@@ -229,13 +245,13 @@
           if m = 0 then K all_tac
           else EVERY' [rtac @{thm Un_cong}, rtac box_equals,
             rtac (nth passive_set_naturals (j - 1) RS sym),
-            rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, etac (morE RS arg_cong), atac],
+            rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
             (fn (i, (set_natural, coalg_set)) =>
               EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
                 etac (morE RS sym RS arg_cong RS trans), atac, rtac set_natural,
                 rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
-                ftac coalg_set, atac, dtac @{thm set_mp}, atac, rtac mp, rtac (mk_conjunctN n i),
+                ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
                 REPEAT_DETERM o etac allE, atac, atac])
             (rev ((1 upto n) ~~ (active_set_naturals ~~ coalg_sets)))])
       (rec_Sucs ~~ (morEs ~~ (map (chop m) set_naturalss ~~ map (drop m) coalg_setss)))] 1;
@@ -252,17 +268,17 @@
     fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), rel_def) =
       EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
         etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
-        rtac (rel_def RS equalityD2 RS @{thm set_mp}),
+        rtac (rel_def RS equalityD2 RS set_mp),
         rtac @{thm relcompI}, rtac @{thm converseI},
         EVERY' (map (fn thm =>
           EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
             rtac CollectI,
             CONJ_WRAP' (fn (i, thm) =>
               if i <= m
-              then EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac subset_trans,
+              then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
                 etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm diagI}]
-              else EVERY' [rtac @{thm ord_eq_le_trans}, rtac trans, rtac thm,
-                rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, atac])
+              else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
+                rtac trans_fun_cong_image_id_id_apply, atac])
             (1 upto (m + n) ~~ set_naturals),
             rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm,
             REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
@@ -271,10 +287,10 @@
     fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), rel_def) =
       EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
         etac allE, etac allE, etac impE, atac,
-        dtac (rel_def RS equalityD1 RS @{thm set_mp}),
+        dtac (rel_def RS equalityD1 RS set_mp),
         REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o dtac Pair_eq_subst_id,
         REPEAT_DETERM o etac conjE,
         hyp_subst_tac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE],
@@ -285,15 +301,15 @@
         REPEAT_DETERM_N m o stac @{thm id_o},
         REPEAT_DETERM_N n o stac @{thm o_id},
         rtac trans, rtac map_cong,
-        REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac @{thm set_mp}, atac],
+        REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac],
         REPEAT_DETERM_N n o rtac refl,
         etac sym, rtac CollectI,
         CONJ_WRAP' (fn (i, thm) =>
           if i <= m
-          then EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI},
-            rtac @{thm diag_fst}, etac @{thm set_mp}, atac]
-          else EVERY' [rtac @{thm ord_eq_le_trans}, rtac trans, rtac thm,
-            rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, atac])
+          then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
+            rtac @{thm diag_fst}, etac set_mp, atac]
+          else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
+            rtac trans_fun_cong_image_id_id_apply, atac])
         (1 upto (m + n) ~~ set_naturals)];
   in
     EVERY' [rtac (bis_def RS trans),
@@ -302,7 +318,7 @@
   end;
 
 fun mk_bis_converse_tac m bis_rel rel_congs rel_converses =
-  EVERY' [stac bis_rel, dtac (bis_rel RS @{thm subst[of _ _ "%x. x"]}),
+  EVERY' [stac bis_rel, dtac (bis_rel RS subst_id),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
       rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
@@ -316,7 +332,7 @@
         rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1;
 
 fun mk_bis_O_tac m bis_rel rel_congs rel_Os =
-  EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS @{thm subst[of _ _ "%x. x"]}),
+  EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS subst_id),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
     CONJ_WRAP' (fn (rel_cong, rel_O) =>
@@ -326,7 +342,7 @@
         REPEAT_DETERM_N (length rel_congs) o rtac refl,
         rtac rel_O,
         etac @{thm relcompE},
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o dtac Pair_eq_subst_id,
         etac conjE, hyp_subst_tac,
         REPEAT_DETERM o etac allE, rtac @{thm relcompI},
         etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1;
@@ -374,18 +390,18 @@
     rtac (mk_nth_conv n i)] 1;
 
 fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
-  EVERY' [rtac @{thm ssubst[of _ _ "%x. x", OF equiv_def]},
+  EVERY' [rtac (@{thm equiv_def} RS ssubst_id),
 
-    rtac conjI, rtac @{thm ssubst[of _ _ "%x. x", OF refl_on_def]},
-    rtac conjI, rtac lsbis_incl, rtac ballI, rtac @{thm set_mp},
+    rtac conjI, rtac (@{thm refl_on_def} RS ssubst_id),
+    rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
     rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
 
-    rtac conjI, rtac @{thm ssubst[of _ _ "%x. x", OF sym_def]},
-    rtac allI, rtac allI, rtac impI, rtac @{thm set_mp},
+    rtac conjI, rtac (@{thm sym_def} RS ssubst_id),
+    rtac allI, rtac allI, rtac impI, rtac set_mp,
     rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
 
-    rtac @{thm ssubst[of _ _ "%x. x", OF trans_def]},
-    rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac @{thm set_mp},
+    rtac (@{thm trans_def} RS ssubst_id),
+    rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp,
     rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
     etac @{thm relcompI}, atac] 1;
 
@@ -397,13 +413,13 @@
       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
         hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
         rtac (mk_sum_casesN n i), rtac CollectI,
-        EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS @{thm ord_eq_le_trans}),
-          etac ((trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]) RS
-            @{thm ord_eq_le_trans})]) passive_sets),
-        CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+        EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
+          etac ((trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]) RS ord_eq_le_trans)])
+          passive_sets),
+        CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
           rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
           rtac conjI,
-          rtac conjI, etac @{thm empty_Shift}, dtac @{thm set_rev_mp},
+          rtac conjI, etac @{thm empty_Shift}, dtac set_rev_mp,
             etac equalityD1, etac CollectD,
           rtac conjI, etac @{thm Shift_clists},
           rtac conjI, etac @{thm Shift_prefCl},
@@ -448,20 +464,20 @@
       rtac @{thm Card_order_ctwo}, rtac @{thm Cinfinite_cexp},
       rtac @{thm ctwo_ordLeq_Cinfinite}, rtac sbd_Cinfinite, rtac sbd_Cinfinite,
       rtac ctrans, rtac @{thm card_of_diff},
-      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_Field_ordIso},
-      rtac @{thm Card_order_cpow}, rtac @{thm ordIso_ordLeq_trans},
+      rtac ordIso_ordLeq_trans, rtac @{thm card_of_Field_ordIso},
+      rtac @{thm Card_order_cpow}, rtac ordIso_ordLeq_trans,
       rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1_Cnotzero},
       if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
       rtac @{thm Card_order_ctwo}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_clists},
-      rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm ordIso_ordLeq_trans},
+      rtac @{thm cexp_mono2_Cnotzero}, rtac ordIso_ordLeq_trans,
       rtac @{thm clists_Cinfinite},
       if n = 1 then rtac sbd_Cinfinite else rtac (sbd_Cinfinite RS @{thm Cinfinite_csum1}),
-      rtac @{thm ordIso_ordLeq_trans}, rtac sbd_sbd, rtac @{thm infinite_ordLeq_cexp},
+      rtac ordIso_ordLeq_trans, rtac sbd_sbd, rtac @{thm infinite_ordLeq_cexp},
       rtac sbd_Cinfinite,
       if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
       rtac @{thm Cnotzero_clists},
-      rtac ballI, rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_Func_Ffunc},
-      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm Func_cexp},
+      rtac ballI, rtac ordIso_ordLeq_trans, rtac @{thm card_of_Func_Ffunc},
+      rtac ordIso_ordLeq_trans, rtac @{thm Func_cexp},
       rtac ctrans, rtac @{thm cexp_mono},
       rtac @{thm ordLeq_ordIso_trans},
       CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1
@@ -481,14 +497,14 @@
       rtac ctrans, rtac @{thm cone_ordLeq_ctwo}, rtac @{thm ordLeq_csum2},
       rtac @{thm Card_order_ctwo}, rtac FalseE, etac @{thm cpow_clists_czero}, atac,
       rtac @{thm card_of_Card_order},
-      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cprod},
+      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod},
       rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
-      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong2_Cnotzero},
+      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cong2_Cnotzero},
       rtac @{thm ordIso_transitive}, rtac @{thm cprod_cong2}, rtac sbd_sbd,
       rtac @{thm cprod_infinite}, rtac sbd_Cinfinite,
       rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_cprod},
       rtac ctrans, rtac @{thm cexp_mono1_Cnotzero},
-      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1},
+      rtac ordIso_ordLeq_trans, rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1},
       rtac @{thm ordIso_transitive},
       REPEAT_DETERM_N m o rtac @{thm csum_cong2},
       rtac sbd_sbd,
@@ -503,7 +519,7 @@
       if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
       rtac @{thm Card_order_ctwo},
       rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac sbd_Card_order,
-      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cprod_ordLeq},
+      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod_ordLeq},
       if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
       rtac sbd_Cinfinite, rtac sbd_Cnotzero, rtac @{thm ordLeq_refl}, rtac sbd_Card_order,
       rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm infinite_ordLeq_cexp},
@@ -512,33 +528,33 @@
       rtac sbd_Cnotzero,
       rtac @{thm card_of_mono1}, rtac subsetI,
       REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac,
-      rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac @{thm set_mp}, rtac equalityD2,
+      rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac set_mp, rtac equalityD2,
       rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),
       rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},
-      hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS @{thm set_mp}),
+      hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
       rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
       CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
-        [rtac (mk_UnN n i), dtac (def RS @{thm subst[of _ _ "%x. x"]}),
+        [rtac (mk_UnN n i), dtac (def RS subst_id),
         REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
         REPEAT_DETERM_N m o (rtac conjI THEN' atac),
-        CONJ_WRAP' (K (EVERY' [etac @{thm ord_eq_le_trans}, rtac subset_trans,
+        CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,
           rtac @{thm subset_UNIV}, rtac equalityD2, rtac @{thm Field_card_order},
           rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs),
       atac] 1
   end;
 
 fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}=
-  EVERY' [dtac (carT_def RS equalityD1 RS @{thm set_mp}),
+  EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
     REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-    dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+    dtac Pair_eq_subst_id,
     etac conjE, hyp_subst_tac,
-    dtac (isNode_def RS @{thm subst[of _ _ "%x. x"]}),
+    dtac (isNode_def RS subst_id),
     REPEAT_DETERM o eresolve_tac [exE, conjE],
-    rtac (equalityD2 RS @{thm set_mp}),
+    rtac (equalityD2 RS set_mp),
     rtac (strT_def RS arg_cong RS trans),
     etac (arg_cong RS trans),
     fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt,
-    rtac set_natural, rtac imageI, etac (equalityD2 RS @{thm set_mp}), rtac CollectI,
+    rtac set_natural, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
     etac @{thm prefCl_Succ}, atac] 1;
 
 fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
@@ -554,10 +570,10 @@
           rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)),
           rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]),
           rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
-        else EVERY' [dtac (carT_def RS equalityD1 RS @{thm set_mp}),
+        else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
           REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
-          dtac conjunct2, dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, etac conjE,
-          hyp_subst_tac, dtac (isNode_def RS @{thm subst[of _ _ "%x. x"]}),
+          dtac conjunct2, dtac Pair_eq_subst_id, etac conjE,
+          hyp_subst_tac, dtac (isNode_def RS subst_id),
           REPEAT_DETERM o eresolve_tac [exE, conjE],
           rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
       (ks ~~ (carT_defs ~~ isNode_defs));
@@ -565,7 +581,7 @@
       dtac (mk_conjunctN n i) THEN'
       CONJ_WRAP' (fn (coalg_set, (carT_set, set_hset_incl_hset)) =>
         EVERY' [rtac impI, etac conjE, etac impE, rtac conjI,
-          rtac (coalgT RS coalg_set RS @{thm set_mp}), atac, etac carT_set, atac, atac,
+          rtac (coalgT RS coalg_set RS set_mp), atac, etac carT_set, atac, atac,
           etac (@{thm shift_def} RS fun_cong RS trans), etac subset_trans,
           rtac set_hset_incl_hset, etac carT_set, atac, atac])
       (coalg_sets ~~ (carT_sets ~~ set_hset_incl_hsets));
@@ -599,18 +615,18 @@
     val n = length Lev_0s;
     val ks = 1 upto n;
   in
-    EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn Lev_0 =>
-        EVERY' (map rtac [@{thm ord_eq_le_trans}, Lev_0, @{thm Nil_clists}])) Lev_0s,
+        EVERY' (map rtac [ord_eq_le_trans, Lev_0, @{thm Nil_clists}])) Lev_0s,
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn (Lev_Suc, to_sbds) =>
-        EVERY' [rtac @{thm ord_eq_le_trans}, rtac Lev_Suc,
+        EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc,
           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
             (fn (i, to_sbd) => EVERY' [rtac subsetI,
               REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
               rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,
-              etac @{thm set_rev_mp}, REPEAT_DETERM o etac allE,
+              etac set_rev_mp, REPEAT_DETERM o etac allE,
               etac (mk_conjunctN n i)])
           (rev (ks ~~ to_sbds))])
       (Lev_Sucs ~~ to_sbdss)] 1
@@ -621,14 +637,14 @@
     val n = length Lev_0s;
     val ks = n downto 1;
   in
-    EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn Lev_0 =>
-        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}),
+        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
           etac @{thm singletonE}, etac ssubst, rtac @{thm list.size(3)}]) Lev_0s,
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn Lev_Suc =>
-        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
+        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
               rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
@@ -644,16 +660,16 @@
     val n = length Lev_0s;
     val ks = n downto 1;
   in
-    EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn Lev_0 =>
-        EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}),
+        EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
           etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefix_Nil[THEN subst, of "%x. x"]},
           hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
           rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
-        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
+        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
               dtac @{thm prefix_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
@@ -697,25 +713,25 @@
     val n = length Lev_0s;
     val ks = 1 upto n;
   in
-    EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
         EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
-          dtac (Lev_0 RS equalityD1 RS @{thm set_mp}), etac @{thm singletonE}, etac ssubst,
-          rtac (rv_Nil RS arg_cong RS @{thm ssubst[of _ _ "%x. x"]}),
-          rtac (mk_sum_casesN n i RS @{thm ssubst[of _ _ "%x. x"]}),
+          dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
+          rtac (rv_Nil RS arg_cong RS ssubst_id),
+          rtac (mk_sum_casesN n i RS ssubst_id),
           CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
       (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) =>
-        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
+        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn (i, (from_to_sbd, coalg_set)) =>
               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
-              rtac (rv_Cons RS arg_cong RS @{thm ssubst[of _ _ "%x. x"]}),
-              rtac (mk_sum_casesN n i RS arg_cong RS trans RS @{thm ssubst[of _ _ "%x. x"]}),
+              rtac (rv_Cons RS arg_cong RS ssubst_id),
+              rtac (mk_sum_casesN n i RS arg_cong RS trans RS ssubst_id),
               etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
-              dtac (mk_conjunctN n i), etac mp, etac conjI, etac @{thm set_rev_mp},
+              dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
               etac coalg_set, atac])
           (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))])
       ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
@@ -726,19 +742,19 @@
     val n = length Lev_0s;
     val ks = 1 upto n;
   in
-    EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
-        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}),
+        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
           etac @{thm singletonE}, hyp_subst_tac,
           CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
             (if i = i'
             then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac,
               CONJ_WRAP' (fn (i'', Lev_0'') =>
                 EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
-                  rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}), rtac (mk_UnN n i''),
+                  rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i''),
                   rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
-                  etac conjI, rtac (Lev_0'' RS equalityD2 RS @{thm set_mp}),
+                  etac conjI, rtac (Lev_0'' RS equalityD2 RS set_mp),
                   rtac @{thm singletonI}])
               (ks ~~ Lev_0s)]
             else etac (mk_InN_not_InM i' i RS notE)))
@@ -746,13 +762,13 @@
       ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
-        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
+        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn (i, from_to_sbd) =>
               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
                 CONJ_WRAP' (fn i' => rtac impI THEN'
                   CONJ_WRAP' (fn i'' =>
-                    EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}),
+                    EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
                       rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnN n i),
                       rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
                       rtac conjI, atac, dtac (sym RS trans RS sym),
@@ -772,20 +788,20 @@
     val n = length Lev_0s;
     val ks = 1 upto n;
   in
-    EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
-        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}),
+        EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
           etac @{thm singletonE}, hyp_subst_tac,
           CONJ_WRAP' (fn i' => rtac impI THEN'
             CONJ_WRAP' (fn i'' => rtac impI  THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
               (if i = i''
               then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
-                dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}), dtac (mk_InN_inject n i),
+                dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
                 hyp_subst_tac,
                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
                   (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
-                    dtac @{thm list.inject[THEN subst, of "%x. x"]} THEN' etac conjE THEN'
+                    dtac list_inject_subst_id THEN' etac conjE THEN'
                     (if k = i'
                     then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
                     else etac (mk_InN_not_InM i' k RS notE)))
@@ -796,19 +812,19 @@
       ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
-        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
+        EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn (i, (from_to_sbd, to_sbd_inj)) =>
               REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac THEN'
               CONJ_WRAP' (fn i' => rtac impI THEN'
                 dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
-                dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}) THEN'
+                dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
                   REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
-                  dtac @{thm list.inject[THEN subst, of "%x. x"]} THEN' etac conjE THEN'
+                  dtac list_inject_subst_id THEN' etac conjE THEN'
                   (if k = i
                   then EVERY' [dtac (mk_InN_inject n i),
-                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS @{thm subst[of _ _ "%x. x"]})),
+                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
                     atac, atac, hyp_subst_tac] THEN'
                     CONJ_WRAP' (fn i'' =>
                       EVERY' [rtac impI, dtac (sym RS trans),
@@ -837,10 +853,10 @@
     fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
       ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_naturals,
         (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
-      EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS @{thm set_mp}),
+      EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
         rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
         rtac conjI,
-          rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS @{thm set_mp}),
+          rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS set_mp),
           rtac @{thm singletonI},
         rtac conjI,
           rtac @{thm UN_least}, rtac Lev_sbd,
@@ -859,8 +875,8 @@
               else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
                 etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)),
               EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
-                EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac (set_natural RS trans),
-                  rtac @{thm trans[OF fun_cong[OF image_id] id_apply]},
+                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
+                  rtac trans_fun_cong_image_id_id_apply,
                   etac set_rv_Lev, TRY o atac, etac conjI, atac])
               (take m set_naturals) set_rv_Levs),
               CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
@@ -883,8 +899,8 @@
               else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
                 etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)),
               EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
-                EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac (set_natural RS trans),
-                  rtac @{thm trans[OF fun_cong[OF image_id] id_apply]},
+                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
+                  rtac trans_fun_cong_image_id_id_apply,
                   etac set_rv_Lev, TRY o atac, etac conjI, atac])
               (take m set_naturals) set_rv_Levs),
               CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
@@ -905,21 +921,21 @@
           etac notE, etac @{thm UN_I[OF UNIV_I]},
         (*root isNode*)
           rtac (isNode_def RS ssubst), rtac exI, rtac conjI, rtac (@{thm if_P} RS trans),
-          rtac length_Lev', rtac (Lev_0 RS equalityD2 RS @{thm set_mp}), rtac @{thm singletonI},
+          rtac length_Lev', rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI},
           CONVERSION (Conv.top_conv
             (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
           if n = 1 then rtac refl else rtac (mk_sum_casesN n i),
           EVERY' (map2 (fn set_natural => fn coalg_set =>
-            EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac (set_natural RS trans),
-              rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, etac coalg_set, atac])
+            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
+              rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
             (take m set_naturals) (take m coalg_sets)),
           CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
             EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
               rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
-              rtac (Lev_0 RS equalityD2 RS @{thm set_mp}), rtac @{thm singletonI}, rtac rv_Nil,
+              rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil,
               atac, rtac subsetI,
               REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
-              rtac set_image_Lev, rtac (Lev_0 RS equalityD2 RS @{thm set_mp}),
+              rtac set_image_Lev, rtac (Lev_0 RS equalityD2 RS set_mp),
               rtac @{thm singletonI}, dtac length_Lev',
               etac @{thm set_mp[OF equalityD1[OF arg_cong[OF
                 trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
@@ -931,7 +947,7 @@
       EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
         rtac (@{thm if_P} RS
           (if n = 1 then map_arg_cong else @{thm sum_case_cong}) RS trans),
-        rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS @{thm set_mp}),
+        rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),
         rtac Lev_0, rtac @{thm singletonI},
         CONVERSION (Conv.top_conv
           (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
@@ -948,28 +964,28 @@
             rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
             CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-                dtac @{thm list.inject[THEN subst, of "%x. x"]}, etac conjE,
+                dtac list_inject_subst_id, etac conjE,
                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
-                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS @{thm subst[of _ _ "%x. x"]})),
+                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
                   atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
                 else etac (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
             rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
-            rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}), rtac (mk_UnN n i'), rtac CollectI,
+            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i'), rtac CollectI,
             REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
             rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI,
             rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI,
             dtac asm_rl, dtac asm_rl, dtac asm_rl,
-            dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}),
+            dtac (Lev_Suc RS equalityD1 RS set_mp),
             CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-                dtac @{thm list.inject[THEN subst, of "%x. x"]}, etac conjE,
+                dtac list_inject_subst_id, etac conjE,
                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
-                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS @{thm subst[of _ _ "%x. x"]})),
+                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
                   atac, atac, hyp_subst_tac, atac]
                 else etac (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
-            rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}), rtac (mk_UnN n i'), rtac CollectI,
+            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i'), rtac CollectI,
             REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
             CONVERSION (Conv.top_conv
               (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
@@ -999,7 +1015,7 @@
     etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans),
     rtac (map_cong RS trans), REPEAT_DETERM_N m o rtac refl,
     EVERY' (map (fn equiv_LSBIS =>
-      EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac @{thm set_mp}, atac])
+      EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac set_mp, atac])
     equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
     etac (sym RS arg_cong RS trans), rtac map_comp_id] 1;
 
@@ -1009,14 +1025,14 @@
       EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
         rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
         EVERY' (map2 (fn set_natural => fn coalgT_set =>
-          EVERY' [rtac conjI, rtac (set_natural RS @{thm ord_eq_le_trans}),
-            rtac @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]},
+          EVERY' [rtac conjI, rtac (set_natural RS ord_eq_le_trans),
+            rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
             etac coalgT_set])
         (take m set_naturals) (take m coalgT_sets)),
         CONJ_WRAP' (fn (equiv_LSBIS, (set_natural, coalgT_set)) =>
-          EVERY' [rtac (set_natural RS @{thm ord_eq_le_trans}),
+          EVERY' [rtac (set_natural RS ord_eq_le_trans),
             rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
-            rtac equiv_LSBIS, etac @{thm set_rev_mp}, etac coalgT_set])
+            rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
         (equiv_LSBISs ~~ drop m (set_naturals ~~ coalgT_sets))])
     ((set_naturalss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
 
@@ -1039,7 +1055,7 @@
       EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_congL,
         EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
           EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
-            etac @{thm set_rev_mp}, rtac coalg_final_set, rtac Rep])
+            etac set_rev_mp, rtac coalg_final_set, rtac Rep])
         Abs_inverses (drop m coalg_final_sets))])
     (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
 
@@ -1050,7 +1066,7 @@
     CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
 
 fun mk_mor_coiter_tac m mor_UNIV unf_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs =
-  EVERY' [rtac @{thm ssubst[of _ _ "%x. x"]}, rtac mor_UNIV,
+  EVERY' [rtac ssubst_id, rtac mor_UNIV,
     CONJ_WRAP' (fn ((Abs_inverse, morE), ((unf_def, coiter_def), (map_comp_id, map_cong))) =>
       EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (unf_def RS trans),
         rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
@@ -1065,7 +1081,7 @@
   let
     val n = length Rep_injects;
   in
-    EVERY' [rtac rev_mp, ftac (bis_def RS @{thm subst[of _ _ "%x. x"]}),
+    EVERY' [rtac rev_mp, ftac (bis_def RS subst_id),
       REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse,
       rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg,
       rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr},
@@ -1076,7 +1092,7 @@
       CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) =>
         EVERY' [rtac subset_trans, rtac @{thm relInvImage_UNIV_relImage}, rtac subset_trans,
           rtac @{thm relInvImage_mono}, rtac subset_trans, etac incl_lsbis,
-          rtac @{thm ord_eq_le_trans}, rtac @{thm sym[OF relImage_relInvImage]},
+          rtac ord_eq_le_trans, rtac @{thm sym[OF relImage_relInvImage]},
           rtac @{thm xt1(3)}, rtac @{thm Sigma_cong},
           rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl,
           rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac,
@@ -1087,13 +1103,13 @@
 
 fun mk_unique_mor_tac raw_coinds bis =
   CONJ_WRAP' (fn raw_coind =>
-    EVERY' [rtac impI, rtac (bis RS raw_coind RS @{thm set_mp} RS @{thm IdD}), atac,
+    EVERY' [rtac impI, rtac (bis RS raw_coind RS set_mp RS @{thm IdD}), atac,
       etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac])
   raw_coinds 1;
 
 fun mk_coiter_unique_mor_tac raw_coinds bis mor coiter_defs =
   CONJ_WRAP' (fn (raw_coind, coiter_def) =>
-    EVERY' [rtac ext, etac (bis RS raw_coind RS @{thm set_mp} RS @{thm IdD}), rtac mor,
+    EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
       rtac @{thm image2_eqI}, rtac refl, rtac (coiter_def RS arg_cong RS trans),
       rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ coiter_defs) 1;
 
@@ -1117,17 +1133,17 @@
     CONJ_WRAP' (K (EVERY' [rtac allI, rtac allI, rtac impI,
       REPEAT_DETERM o etac allE, etac mp, etac CollectE, etac @{thm splitD}])) ks,
     rtac impI, REPEAT_DETERM o etac conjE,
-    CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac @{thm set_mp},
+    CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
       rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
 
 fun mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids =
   EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts rel_coinduct),
     EVERY' (map2 (fn rel_mono => fn rel_Id =>
       EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
-        etac disjE, etac mp, atac, hyp_subst_tac, rtac (rel_mono RS @{thm set_mp}),
+        etac disjE, etac mp, atac, hyp_subst_tac, rtac (rel_mono RS set_mp),
         REPEAT_DETERM_N m o rtac @{thm subset_refl},
         REPEAT_DETERM_N (length rel_monos) o rtac @{thm Id_subset},
-        rtac (rel_Id RS equalityD2 RS @{thm set_mp}), rtac @{thm IdI}])
+        rtac (rel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
     rel_monos rel_Ids),
     rtac impI, REPEAT_DETERM o etac conjE,
     CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_Ids] 1;
@@ -1149,7 +1165,7 @@
       ks,
       rtac impI,
       CONJ_WRAP' (fn i => EVERY' [rtac impI, dtac (mk_conjunctN n i),
-        rtac @{thm subst[OF pair_in_Id_conv]}, etac @{thm set_mp},
+        rtac @{thm subst[OF pair_in_Id_conv]}, etac set_mp,
         rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
   end;
 
@@ -1162,7 +1178,7 @@
         etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
         rtac exI, rtac conjI, etac conjI, atac,
         CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
-          rtac disjI2, rtac @{thm diagE}, etac @{thm set_mp}, atac])) ks])
+          rtac disjI2, rtac @{thm diagE}, etac set_mp, atac])) ks])
     ks),
     rtac impI, REPEAT_DETERM o etac conjE,
     CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
@@ -1208,10 +1224,6 @@
         replicate n (@{thm o_id} RS fun_cong))))
     maps map_comps map_congs)] 1;
 
-val o_apply_trans_sym = o_apply RS trans RS sym;
-val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;
-val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
-
 fun mk_mcong_tac m coinduct_tac map_comp's map_simps map_congs set_naturalss set_hsetss
   set_hset_hsetsss =
   let
@@ -1233,7 +1245,7 @@
          REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
          CONJ_WRAP' (fn (set_natural, set_hset_hsets) =>
            EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD},
-             etac @{thm set_rev_mp}, rtac @{thm ord_eq_le_trans}, rtac set_natural,
+             etac set_rev_mp, rtac ord_eq_le_trans, rtac set_natural,
              rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE,
              REPEAT_DETERM o etac conjE,
              CONJ_WRAP' (fn set_hset_hset =>
@@ -1257,7 +1269,7 @@
   let
     val n = length map_simps;
   in
-    EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac allI, SELECT_GOAL (Local_Defs.unfold_tac ctxt rec_0s),
       CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
       REPEAT_DETERM o rtac allI,
@@ -1280,13 +1292,13 @@
   let
     val n = length rec_0s;
   in
-    EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn rec_0 => EVERY' (map rtac [@{thm ordIso_ordLeq_trans},
+      CONJ_WRAP' (fn rec_0 => EVERY' (map rtac [ordIso_ordLeq_trans,
         @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s,
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY'
-        [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, rtac rec_Suc,
+        [rtac ordIso_ordLeq_trans, rtac @{thm card_of_ordIso_subst}, rtac rec_Suc,
         rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_sbds (j - 1)),
         REPEAT_DETERM_N (n - 1) o rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
         EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac @{thm UNION_Cinfinite_bound},
@@ -1296,8 +1308,8 @@
   end;
 
 fun mk_set_bd_tac sbd_Cinfinite hset_def col_bd =
-  EVERY' (map rtac [@{thm ordIso_ordLeq_trans}, @{thm card_of_ordIso_subst}, hset_def,
-    ctrans, @{thm UNION_Cinfinite_bound}, @{thm ordIso_ordLeq_trans}, @{thm card_of_nat},
+  EVERY' (map rtac [ordIso_ordLeq_trans, @{thm card_of_ordIso_subst}, hset_def,
+    ctrans, @{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat},
     @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
     ctrans, @{thm infinite_ordLeq_cexp}, sbd_Cinfinite, @{thm cexp_ordLeq_ccexp}]) 1;
 
@@ -1307,24 +1319,24 @@
     val n = length isNode_hsets;
     val in_hin_tac = rtac CollectI THEN'
       CONJ_WRAP' (fn mor_hset => EVERY' (map etac
-        [mor_hset OF [coalgT, mor_T_final] RS sym RS @{thm ord_eq_le_trans},
-        arg_cong RS sym RS @{thm ord_eq_le_trans},
-        mor_hset OF [tcoalg, mor_Rep, UNIV_I] RS @{thm ord_eq_le_trans}])) mor_hsets;
+        [mor_hset OF [coalgT, mor_T_final] RS sym RS ord_eq_le_trans,
+        arg_cong RS sym RS ord_eq_le_trans,
+        mor_hset OF [tcoalg, mor_Rep, UNIV_I] RS ord_eq_le_trans])) mor_hsets;
   in
     EVERY' [rtac (Thm.permute_prems 0 1 @{thm ordLeq_transitive}), rtac ctrans,
-      rtac @{thm card_of_image}, rtac @{thm ordIso_ordLeq_trans},
+      rtac @{thm card_of_image}, rtac ordIso_ordLeq_trans,
       rtac @{thm card_of_ordIso_subst}, rtac @{thm sym[OF proj_image]}, rtac ctrans,
       rtac @{thm card_of_image}, rtac ctrans, rtac card_of_carT, rtac @{thm cexp_mono2_Cnotzero},
       rtac @{thm cexp_ordLeq_ccexp},  rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
       rtac @{thm Cnotzero_cexp}, rtac sbd_Cnotzero, rtac sbd_Card_order,
       rtac @{thm card_of_mono1}, rtac subsetI, rtac @{thm image_eqI}, rtac sym,
       rtac Rep_inverse, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
-      rtac @{thm set_mp}, rtac equalityD2, rtac @{thm sym[OF proj_image]}, rtac imageE,
-      rtac @{thm set_rev_mp}, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2,
+      rtac set_mp, rtac equalityD2, rtac @{thm sym[OF proj_image]}, rtac imageE,
+      rtac set_rev_mp, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2,
       rtac @{thm proj_image},  rtac @{thm image_eqI}, atac,
-      ftac (carT_def RS equalityD1 RS @{thm set_mp}),
+      ftac (carT_def RS equalityD1 RS set_mp),
       REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
-      rtac (carT_def RS equalityD2 RS @{thm set_mp}), rtac CollectI, REPEAT_DETERM o rtac exI,
+      rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI,
       rtac conjI, rtac refl, rtac conjI, etac conjI, etac conjI, etac conjI, rtac conjI,
       rtac ballI, dtac bspec, atac, REPEAT_DETERM o etac conjE, rtac conjI,
       CONJ_WRAP_GEN' (etac disjE) (fn (i, isNode_hset) =>
@@ -1371,8 +1383,8 @@
       rtac CollectI,
       REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}),
       CONJ_WRAP' (fn set_natural =>
-        EVERY' [rtac @{thm ord_eq_le_trans}, rtac trans, rtac set_natural,
-          rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, atac])
+        EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_natural,
+          rtac trans_fun_cong_image_id_id_apply, atac])
       (drop m set_naturals)])
   (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1;
 
@@ -1415,10 +1427,10 @@
     val n = length rec_0s;
     val ks = n downto 1;
   in
-    EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}),
+    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn thm => EVERY'
-        [rtac impI, rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
+        [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn (rec_Suc, ((coiter, set_naturals), (map_wpull, pickWP_assms_tac))) =>
         EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
@@ -1427,23 +1439,23 @@
           EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
           pickWP_assms_tac,
           rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
-          rtac @{thm ord_eq_le_trans}, rtac rec_Suc,
+          rtac ord_eq_le_trans, rtac rec_Suc,
           rtac @{thm Un_least},
           SELECT_GOAL (Local_Defs.unfold_tac ctxt [coiter, nth set_naturals (j - 1),
             @{thm prod.cases}]),
-          etac @{thm ord_eq_le_trans[OF trans [OF fun_cong[OF image_id] id_apply]]},
+          etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) =>
             EVERY' [rtac @{thm UN_least},
               SELECT_GOAL (Local_Defs.unfold_tac ctxt [coiter, set_natural, @{thm prod.cases}]),
               etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
-              dtac (mk_conjunctN n i), etac mp, etac @{thm set_mp}, atac])
+              dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
           (ks ~~ rev (drop m set_naturals))])
       (rec_Sucs ~~ ((coiters ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   end;
 
 fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
   mor_unique pick_cols hset_defs =
-  EVERY' [rtac @{thm ssubst[of _ _ "%x. x", OF wpull_def]}, REPEAT_DETERM o rtac allI, rtac impI,
+  EVERY' [rtac (@{thm wpull_def} RS ssubst_id), REPEAT_DETERM o rtac allI, rtac impI,
     REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI,
     rtac box_equals, rtac mor_unique,
     rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
@@ -1459,7 +1471,7 @@
     rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm snd_conv},
     rtac CollectI,
     CONJ_WRAP' (fn (pick, def) =>
-      EVERY' [rtac (def RS @{thm ord_eq_le_trans}), rtac @{thm UN_least},
+      EVERY' [rtac (def RS ord_eq_le_trans), rtac @{thm UN_least},
         rtac pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
         rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
         rtac @{thm prod_caseI}, etac conjI, etac conjI, atac])
@@ -1468,7 +1480,7 @@
 fun mk_wit_tac n unf_flds set_simp wit coind_wits {context = ctxt, prems = _} =
   ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
   REPEAT_DETERM (atac 1 ORELSE
-    EVERY' [dtac @{thm set_rev_mp}, rtac equalityD1, resolve_tac set_simp,
+    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
     K (Local_Defs.unfold_tac ctxt unf_flds),
     REPEAT_DETERM_N n o etac UnE,
     REPEAT_DETERM o
@@ -1476,7 +1488,7 @@
         (eresolve_tac wit ORELSE'
         (dresolve_tac wit THEN'
           (etac FalseE ORELSE'
-          EVERY' [hyp_subst_tac, dtac @{thm set_rev_mp}, rtac equalityD1, resolve_tac set_simp,
+          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
             K (Local_Defs.unfold_tac ctxt unf_flds), REPEAT_DETERM_N n o etac UnE]))))] 1);
 
 fun mk_coind_wit_tac induct coiters set_nats wits {context = ctxt, prems = _} =
@@ -1497,12 +1509,12 @@
       EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
         EVERY' (map2 (fn set_natural => fn set_incl =>
-          EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac set_natural,
-            rtac @{thm ord_eq_le_trans}, rtac @{thm trans[OF fun_cong[OF image_id] id_apply]},
+          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
+            rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
             etac (set_incl RS @{thm subset_trans})])
         passive_set_naturals set_incls),
         CONJ_WRAP' (fn (in_Jrel, (set_natural, set_set_incls)) =>
-          EVERY' [rtac @{thm ord_eq_le_trans}, rtac set_natural, rtac @{thm image_subsetI},
+          EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
             rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
             CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls,
             rtac conjI, rtac refl, rtac refl])
@@ -1517,15 +1529,14 @@
       EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
         CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
-          EVERY' [rtac @{thm ord_eq_le_trans}, rtac set_simp, rtac @{thm Un_least},
-            rtac @{thm ord_eq_le_trans}, rtac box_equals, rtac passive_set_natural,
-            rtac (unf_fld RS sym RS arg_cong), rtac @{thm trans[OF fun_cong[OF image_id] id_apply]},
-            atac,
+          EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
+            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural,
+            rtac (unf_fld RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
-              (fn (active_set_natural, in_Jrel) => EVERY' [rtac @{thm ord_eq_le_trans},
+              (fn (active_set_natural, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
                 rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
                 rtac active_set_natural, rtac (unf_fld RS sym RS arg_cong), rtac @{thm UN_least},
-                dtac @{thm set_rev_mp}, etac @{thm image_mono}, etac imageE,
+                dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
                 dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1),
                 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
                 dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
@@ -1536,7 +1547,7 @@
         REPEAT_DETERM_N 2 o EVERY'[rtac (unf_inject RS iffD1), rtac trans, rtac map_simp,
           rtac box_equals, rtac map_comp, rtac (unf_fld RS sym RS arg_cong), rtac trans,
           rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
-          EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac @{thm set_rev_mp}, atac,
+          EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1), dtac @{thm someI_ex},
             REPEAT_DETERM o etac conjE, atac]) in_Jrels),
           atac]]