more antiquotations;

--- a/src/HOL/Product_Type.thy	Tue Jul 05 22:23:17 2016 +0200
+++ b/src/HOL/Product_Type.thy	Tue Jul 05 22:47:48 2016 +0200
@@ -1362,8 +1362,10 @@
                         (K (EVERY
                           [resolve_tac ctxt [eq_reflection] 1,
                            resolve_tac ctxt @{thms subset_antisym} 1,
-                           resolve_tac ctxt [subsetI] 1, dresolve_tac ctxt [CollectD] 1, simp,
-                           resolve_tac ctxt [subsetI] 1, resolve_tac ctxt [CollectI] 1, simp])))
+                           resolve_tac ctxt @{thms subsetI} 1,
+                           dresolve_tac ctxt @{thms CollectD} 1, simp,
+                           resolve_tac ctxt @{thms subsetI} 1,
+                           resolve_tac ctxt @{thms CollectI} 1, simp])))
                     end
                   else NONE)
           | _ => NONE)

--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Jul 05 22:23:17 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Jul 05 22:47:48 2016 +0200
@@ -1735,7 +1735,7 @@
               unfold_thms_tac ctxt [#pred_set axioms] THEN
               HEADGOAL (EVERY' [REPEAT_DETERM o etac ctxt conjE,
                 etac ctxt (Lazy.force map_cong) THEN_ALL_NEW
-                  (etac ctxt bspec THEN' assume_tac ctxt)]))
+                  (etac ctxt @{thm bspec} THEN' assume_tac ctxt)]))
             |> Thm.close_derivation
           end;
 

--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Tue Jul 05 22:23:17 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Tue Jul 05 22:47:48 2016 +0200
@@ -64,11 +64,11 @@
 fun mk_in_mono_tac ctxt n =
   if n = 0 then rtac ctxt subset_UNIV 1
   else
-   (rtac ctxt subsetI THEN' rtac ctxt CollectI) 1 THEN
-   REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN
+   (rtac ctxt @{thm subsetI} THEN' rtac ctxt @{thm CollectI}) 1 THEN
+   REPEAT_DETERM (eresolve_tac ctxt @{thms CollectE conjE} 1) THEN
    REPEAT_DETERM_N (n - 1)
-     ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' assume_tac ctxt) 1) THEN
-   (etac ctxt subset_trans THEN' assume_tac ctxt) 1;
+     ((rtac ctxt conjI THEN' etac ctxt @{thm subset_trans} THEN' assume_tac ctxt) 1) THEN
+   (etac ctxt @{thm subset_trans} THEN' assume_tac ctxt) 1;
 
 fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong =
   let
@@ -109,13 +109,12 @@
       resolve_tac ctxt @{thms refl Grp_UNIV_idI[OF refl]} 1
     else
       EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I},
-        REPEAT_DETERM o eresolve_tac ctxt
-          [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
         hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp,
           rtac ctxt map_cong0,
         REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD},
           etac ctxt @{thm set_mp}, assume_tac ctxt],
-        rtac ctxt CollectI,
+        rtac ctxt @{thm CollectI},
         CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
           rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in},
           etac ctxt @{thm set_mp}, assume_tac ctxt])
@@ -127,8 +126,8 @@
           EVERY' [rtac ctxt @{thm GrpI},
             rtac ctxt (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]),
             REPEAT_DETERM_N n o rtac ctxt (convol RS fun_cong),
-            REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
-            rtac ctxt CollectI,
+            REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE},
+            rtac ctxt @{thm CollectI},
             CONJ_WRAP' (fn thm =>
               EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
                 rtac ctxt @{thm convol_mem_GrpI}, etac ctxt set_mp, assume_tac ctxt])
@@ -141,7 +140,8 @@
   rtac ctxt (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
   (if n = 0 then SELECT_GOAL (unfold_thms_tac ctxt (no_refl [map_id0])) THEN' rtac ctxt refl
   else EVERY' [rtac ctxt @{thm arg_cong2[of _ _ _ _ "Grp"]},
-    rtac ctxt @{thm equalityI}, rtac ctxt subset_UNIV, rtac ctxt subsetI, rtac ctxt CollectI,
+    rtac ctxt @{thm equalityI}, rtac ctxt subset_UNIV,
+    rtac ctxt @{thm subsetI}, rtac ctxt @{thm CollectI},
     CONJ_WRAP' (K (rtac ctxt subset_UNIV)) (1 upto n), rtac ctxt map_id0])) 1;
 
 fun mk_rel_map0_tac ctxt live rel_compp rel_conversep rel_Grp map_id =
@@ -156,10 +156,10 @@
       Goal.conjunction_tac 1 THEN
       unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
       TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI},
-        resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
+        resolve_tac ctxt [map_id, refl], rtac ctxt @{thm CollectI},
         CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI},
         assume_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
-        resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
+        resolve_tac ctxt [map_id, refl], rtac ctxt @{thm CollectI},
         CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks,
         REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
         dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt])
@@ -187,11 +187,11 @@
     else
       EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I},
         REPEAT_DETERM o
-          eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+          eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
         hyp_subst_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI},
         EVERY' (map (fn thm => EVERY' [rtac ctxt @{thm GrpI}, rtac ctxt sym, rtac ctxt trans,
           rtac ctxt map_cong0, REPEAT_DETERM_N n o rtac ctxt thm,
-          rtac ctxt (map_comp RS sym), rtac ctxt CollectI,
+          rtac ctxt (map_comp RS sym), rtac ctxt @{thm CollectI},
           CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
             etac ctxt @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
   end;
@@ -204,7 +204,7 @@
 fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
   let
     val n = length set_maps;
-    fun in_tac nthO_in = rtac ctxt CollectI THEN'
+    fun in_tac nthO_in = rtac ctxt @{thm CollectI} THEN'
         CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
           rtac ctxt @{thm image_subsetI}, rtac ctxt nthO_in, etac ctxt set_mp, assume_tac ctxt]) set_maps;
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
@@ -215,8 +215,7 @@
     if null set_maps then rtac ctxt (rel_eq RS @{thm leq_OOI}) 1
     else
       EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm predicate2I},
-        REPEAT_DETERM o
-          eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE exE conjE GrpE relcomppE conversepE},
         hyp_subst_tac ctxt,
         rtac ctxt @{thm relcomppI}, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
         rtac ctxt trans, rtac ctxt map_comp, rtac ctxt sym, rtac ctxt map_cong0,
@@ -224,7 +223,7 @@
         in_tac @{thm fstOp_in},
         rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
         REPEAT_DETERM_N n o EVERY' [rtac ctxt trans, rtac ctxt o_apply,
-          rtac ctxt ballE, rtac ctxt subst,
+          rtac ctxt @{thm ballE}, rtac ctxt subst,
           rtac ctxt @{thm csquare_def}, rtac ctxt @{thm csquare_fstOp_sndOp}, assume_tac ctxt,
           etac ctxt notE, etac ctxt set_mp, assume_tac ctxt],
         in_tac @{thm fstOp_in},
@@ -241,7 +240,7 @@
   if null set_maps then assume_tac ctxt 1
   else
     unfold_tac ctxt [in_rel] THEN
-    REPEAT_DETERM (eresolve_tac ctxt [exE, CollectE, conjE] 1) THEN
+    REPEAT_DETERM (eresolve_tac ctxt @{thms exE CollectE conjE} 1) THEN
     hyp_subst_tac ctxt 1 THEN
     EVERY' [rtac ctxt exI, rtac ctxt @{thm conjI[OF CollectI conjI[OF refl refl]]},
       CONJ_WRAP' (fn thm =>
@@ -266,18 +265,20 @@
 fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =
   let
     val n = length set_maps;
-    val in_tac = if n = 0 then rtac ctxt UNIV_I else
-      rtac ctxt CollectI THEN' CONJ_WRAP' (fn thm =>
-        etac ctxt (thm RS
-          @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
-      set_maps;
+    val in_tac =
+      if n = 0 then rtac ctxt @{thm UNIV_I}
+      else
+        rtac ctxt @{thm CollectI} THEN' CONJ_WRAP' (fn thm =>
+          etac ctxt (thm RS
+            @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
+        set_maps;
   in
     REPEAT_DETERM_N n (HEADGOAL (rtac ctxt rel_funI)) THEN
     unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
     HEADGOAL (EVERY' [rtac ctxt @{thm order_trans}, rtac ctxt rel_mono,
       REPEAT_DETERM_N n o assume_tac ctxt,
       rtac ctxt @{thm predicate2I}, dtac ctxt (in_rel RS iffD1),
-      REPEAT_DETERM o eresolve_tac ctxt [exE, CollectE, conjE], hyp_subst_tac ctxt,
+      REPEAT_DETERM o eresolve_tac ctxt @{thms exE CollectE conjE}, hyp_subst_tac ctxt,
       rtac ctxt @{thm vimage2pI}, rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, in_tac,
       rtac ctxt conjI,
       EVERY' (map (fn convol =>
@@ -322,9 +323,11 @@
         rtac ctxt @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN
       unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN
       unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN
-      EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst, rtac ctxt subsetI,
+      EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst,
+        rtac ctxt @{thm subsetI},
         Method.insert_tac ctxt inserts, REPEAT_DETERM o dtac ctxt meta_spec,
-        REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1], etac ctxt CollectE,
+        REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1],
+        etac ctxt @{thm CollectE},
         if live = 1 then K all_tac
         else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE,
         rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}), rtac ctxt @{thm SigmaI}, rtac ctxt @{thm UNIV_I},
@@ -337,8 +340,10 @@
         REPEAT_DETERM_N (2 * live) o assume_tac ctxt,
         REPEAT_DETERM_N live o rtac ctxt (@{thm prod.case} RS trans),
         rtac ctxt refl,
-        rtac ctxt @{thm surj_imp_ordLeq}, rtac ctxt subsetI, rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}),
-        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
+        rtac ctxt @{thm surj_imp_ordLeq},
+        rtac ctxt @{thm subsetI},
+        rtac ctxt (Drule.rotate_prems 1 @{thm image_eqI}),
+        REPEAT_DETERM o eresolve_tac ctxt @{thms CollectE conjE}, rtac ctxt @{thm CollectI},
         CONJ_WRAP' (fn thm =>
           rtac ctxt (thm RS ord_eq_le_trans) THEN' etac ctxt @{thm subset_trans[OF image_mono Un_upper1]})
         set_maps,
@@ -350,7 +355,8 @@
 fun mk_trivial_wit_tac ctxt wit_defs set_maps =
   unfold_thms_tac ctxt wit_defs THEN
   HEADGOAL (EVERY' (map (fn thm =>
-    dtac ctxt (thm RS equalityD1 RS set_mp) THEN' etac ctxt imageE THEN' assume_tac ctxt) set_maps)) THEN
+    dtac ctxt (thm RS @{thm equalityD1} RS set_mp) THEN'
+    etac ctxt @{thm imageE} THEN' assume_tac ctxt) set_maps)) THEN
   ALLGOALS (assume_tac ctxt);
 
 fun mk_set_transfer_tac ctxt in_rel set_maps =
@@ -360,9 +366,10 @@
     @{thms exE conjE CollectE}))) THEN
   HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
     rtac ctxt @{thm rel_setI}) THEN
-  REPEAT (HEADGOAL (etac ctxt imageE THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN'
+  REPEAT (HEADGOAL (etac ctxt @{thm imageE} THEN' dtac ctxt @{thm set_mp} THEN' assume_tac ctxt THEN'
     REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN'
-    rtac ctxt bexI THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt imageI))) set_maps);
+    rtac ctxt @{thm bexI} THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt @{thm imageI})))
+    set_maps);
 
 fun mk_rel_cong_tac ctxt (eqs, prems) mono =
   let
@@ -391,7 +398,7 @@
 
 fun mk_pred_transfer_tac ctxt n in_rel pred_map pred_cong =
   HEADGOAL (EVERY' [REPEAT_DETERM_N (n + 1) o rtac ctxt rel_funI, dtac ctxt (in_rel RS iffD1),
-    REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt,
+    REPEAT_DETERM o eresolve_tac ctxt @{thms exE conjE CollectE}, hyp_subst_tac ctxt,
     rtac ctxt (box_equals OF [@{thm _}, pred_map RS sym, pred_map RS sym]),
     rtac ctxt (refl RS pred_cong), REPEAT_DETERM_N n o
       (etac ctxt @{thm rel_fun_Collect_case_prodD[where B="op ="]} THEN_ALL_NEW assume_tac ctxt)]);

--- a/src/HOL/Tools/BNF/bnf_tactics.ML	Tue Jul 05 22:23:17 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Tue Jul 05 22:47:48 2016 +0200
@@ -62,7 +62,7 @@
 
 (* Theorems for open typedefs with UNIV as representing set *)
 
-fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I);
+fun mk_Abs_inj_thm inj = inj OF (replicate 2 @{thm UNIV_I});
 fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac ctxt surj THEN' etac ctxt exI) 1)
   (Abs_inj_thm RS @{thm bijI'});
 
@@ -96,11 +96,11 @@
 
 fun mk_map_cong0_tac ctxt m map_cong0 =
   EVERY' [rtac ctxt mp, rtac ctxt map_cong0,
-    CONJ_WRAP' (K (rtac ctxt ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
+    CONJ_WRAP' (K (rtac ctxt @{thm ballI} THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
 
 fun mk_map_cong0L_tac ctxt passive map_cong0 map_id =
   (rtac ctxt trans THEN' rtac ctxt map_cong0 THEN' EVERY' (replicate passive (rtac ctxt refl))) 1 THEN
-  REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt bspec, assume_tac ctxt,
+  REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt @{thm bspec}, assume_tac ctxt,
       rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN
   rtac ctxt map_id 1;
 

--- a/src/HOL/Tools/BNF/bnf_util.ML	Tue Jul 05 22:23:17 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Tue Jul 05 22:47:48 2016 +0200
@@ -420,12 +420,12 @@
 val mk_rel_funDN_rotated = rotate_prems ~1 oo mk_rel_funDN;
 
 local
-  fun mk_Un_upper' 0 = subset_refl
+  fun mk_Un_upper' 0 = @{thm subset_refl}
     | mk_Un_upper' 1 = @{thm Un_upper1}
     | mk_Un_upper' k = Library.foldr (op RS o swap)
       (replicate (k - 1) @{thm subset_trans[OF Un_upper1]}, @{thm Un_upper1});
 in
-  fun mk_Un_upper 1 1 = subset_refl
+  fun mk_Un_upper 1 1 = @{thm subset_refl}
     | mk_Un_upper n 1 = mk_Un_upper' (n - 2) RS @{thm subset_trans[OF Un_upper1]}
     | mk_Un_upper n m = mk_Un_upper' (n - m) RS @{thm subset_trans[OF Un_upper2]};
 end;

--- a/src/HOL/Tools/inductive_set.ML	Tue Jul 05 22:23:17 2016 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Tue Jul 05 22:47:48 2016 +0200
@@ -66,7 +66,7 @@
           | decomp _ = NONE;
         val simp =
           full_simp_tac
-            (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm case_prod_conv}]) 1;
+            (put_simpset HOL_basic_ss ctxt addsimps @{thms mem_Collect_eq case_prod_conv}) 1;
         fun mk_rew t = (case strip_abs_vars t of
             [] => NONE
           | xs => (case decomp (strip_abs_body t) of
@@ -77,13 +77,17 @@
                   (K (EVERY
                     [resolve_tac ctxt [eq_reflection] 1,
                      REPEAT (resolve_tac ctxt @{thms ext} 1),
-                     resolve_tac ctxt [iffI] 1,
-                     EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [IntI] 1, simp, simp,
-                       eresolve_tac ctxt [IntE] 1, resolve_tac ctxt [conjI] 1, simp, simp] ORELSE
-                     EVERY [eresolve_tac ctxt [disjE] 1, resolve_tac ctxt [UnI1] 1, simp,
-                       resolve_tac ctxt [UnI2] 1, simp,
-                       eresolve_tac ctxt [UnE] 1, resolve_tac ctxt [disjI1] 1, simp,
-                       resolve_tac ctxt [disjI2] 1, simp]])))
+                     resolve_tac ctxt @{thms iffI} 1,
+                     EVERY [eresolve_tac ctxt @{thms conjE} 1,
+                       resolve_tac ctxt @{thms IntI} 1, simp, simp,
+                       eresolve_tac ctxt @{thms IntE} 1,
+                       resolve_tac ctxt @{thms conjI} 1, simp, simp] ORELSE
+                     EVERY [eresolve_tac ctxt @{thms disjE} 1,
+                       resolve_tac ctxt @{thms UnI1} 1, simp,
+                       resolve_tac ctxt @{thms UnI2} 1, simp,
+                       eresolve_tac ctxt @{thms UnE} 1,
+                       resolve_tac ctxt @{thms disjI1} 1, simp,
+                       resolve_tac ctxt @{thms disjI2} 1, simp]])))
                   handle ERROR _ => NONE))
       in
         (case strip_comb (Thm.term_of ct) of
@@ -235,9 +239,10 @@
                   HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
           end)
   in
-    Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm case_prod_conv}]
-      addsimprocs [@{simproc Collect_mem}]) thm'' |>
-        zero_var_indexes |> eta_contract_thm ctxt (equal p)
+    Simplifier.simplify
+      (put_simpset HOL_basic_ss ctxt addsimps @{thms mem_Collect_eq case_prod_conv}
+        addsimprocs [@{simproc Collect_mem}]) thm''
+      |> zero_var_indexes |> eta_contract_thm ctxt (equal p)
   end;
 
 
@@ -342,7 +347,7 @@
     thm |>
     Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
-      [to_pred_simproc (mem_Collect_eq :: @{thm case_prod_conv} :: to_pred_simps)]) |>
+      [to_pred_simproc (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: to_pred_simps)]) |>
     eta_contract_thm ctxt (is_pred pred_arities) |>
     Rule_Cases.save thm
   end;
@@ -445,7 +450,7 @@
       end) |> split_list |>> split_list;
     val eqns' = eqns @
       map (Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)
-        (mem_Collect_eq :: @{thm case_prod_conv} :: to_pred_simps);
+        (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: to_pred_simps);
 
     (* predicate version of the introduction rules *)
     val intros' =
@@ -486,7 +491,7 @@
                   list_comb (c, params))))))
             (K (REPEAT (resolve_tac lthy @{thms ext} 1) THEN
               simp_tac (put_simpset HOL_basic_ss lthy addsimps
-                [def, mem_Collect_eq, @{thm case_prod_conv}]) 1))
+                [def, @{thm mem_Collect_eq}, @{thm case_prod_conv}]) 1))
         in
           lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
             [Attrib.internal (K pred_set_conv_att)]),