# HG changeset patch
# User wenzelm
# Date 1394227858 -3600
# Node ID 41c6b99c5fb7d5554332d339acb62a51907de6cc
# Parent  55827fc7c0dd36d47fd6c5dee66017a6d886822d
more antiquotations;

diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Fun.thy	Fri Mar 07 22:30:58 2014 +0100
@@ -895,7 +895,7 @@
           SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
             (fn _ =>
               rtac eq_reflection 1 THEN
-              rtac ext 1 THEN
+              rtac @{thm ext} 1 THEN
               simp_tac (put_simpset ss ctxt) 1))
     end
 in proc end
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -1723,8 +1723,8 @@
                 (finite_thss ~~ finite_ctxt_ths) @
             maps (fn ((_, idxss), elim) => maps (fn idxs =>
               [full_simp_tac (put_simpset HOL_ss context addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1,
-               REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
-               rtac ex1I 1,
+               REPEAT_DETERM (eresolve_tac @{thms conjE ex1E} 1),
+               rtac @{thm ex1I} 1,
                (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
                rotate_tac ~1 1,
                ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -241,7 +241,7 @@
 (* applies the ext-rule such that      *)
 (*                                     *)
 (*    f = g   goes to  /\x. f x = g x  *)
-fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
+fun ext_fun_tac i = ("extensionality expansion of functions", rtac @{thm ext} i);
 
 
 (* perm_extend_simp_tac_i is perm_simp plus additional tactics        *)
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/BNF/bnf_comp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -55,17 +55,17 @@
   rtac refl 1;
 
 fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s =
-  EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
+  EVERY' ([rtac @{thm ext}, rtac (Gmap_cong0 RS trans)] @
     map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1;
 
 fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s =
-  EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
+  EVERY' ([rtac @{thm ext}, rtac sym, rtac trans_o_apply,
     rtac (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), rtac Gmap_cong0] @
     map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1;
 
 fun mk_comp_set_map0_tac ctxt set'_eq_set Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
   unfold_thms_tac ctxt [set'_eq_set] THEN
-  EVERY' ([rtac ext] @
+  EVERY' ([rtac @{thm ext}] @
     replicate 3 (rtac trans_o_apply) @
     [rtac (arg_cong_Union RS trans),
      rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
@@ -79,7 +79,7 @@
      rtac @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]},
      rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
      [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]},
-        rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
+        rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac @{thm ext}, rtac trans_o_apply,
         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;
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -84,7 +84,8 @@
         hyp_subst_tac ctxt,
         rtac @{thm relcomppI}, rtac @{thm conversepI},
         EVERY' (map2 (fn convol => fn map_id0 =>
-          EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]),
+          EVERY' [rtac @{thm GrpI},
+            rtac (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]),
             REPEAT_DETERM_N n o rtac (convol RS fun_cong),
             REPEAT_DETERM o eresolve_tac [CollectE, conjE],
             rtac CollectI,
@@ -203,7 +204,7 @@
       rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, in_tac,
       rtac conjI,
       EVERY' (map (fn convol =>
-        rtac (box_equals OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
+        rtac (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
         REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})])
   end;
 
@@ -254,7 +255,7 @@
           (K (etac @{thm If_the_inv_into_in_Func} THEN' atac)) set_maps,
         rtac sym,
         rtac (Drule.rotate_prems 1
-           ((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
+           ((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
              map_comp RS sym, map_id]) RSN (2, trans))),
         REPEAT_DETERM_N (2 * live) o atac,
         REPEAT_DETERM_N live o rtac (@{thm prod.case} RS trans),
@@ -265,7 +266,7 @@
           rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]})
         set_maps,
         rtac sym,
-        rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
+        rtac (@{thm box_equals} OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
            map_comp RS sym, map_id])] 1
   end;
 
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -525,7 +525,8 @@
     val map_cong_active_args2 = replicate n (if is_rec
       then case_fp fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id}
       else case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong);
-    fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
+    fun mk_map_congs passive active =
+      map (fn thm => thm OF (passive @ active) RS @{thm ext}) map_cong0s;
     val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
     val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;
     
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -140,7 +140,7 @@
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
        sum.case} @ mapsx @ map_comps @ map_idents))) ORELSE'
     fo_rtac @{thm cong} ctxt ORELSE'
-    rtac ext));
+    rtac @{thm ext}));
 
 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
   HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -145,7 +145,7 @@
 fun mk_mor_UNIV_tac morEs mor_def =
   let
     val n = length morEs;
-    fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
+    fun mor_tac morE = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, etac morE,
       rtac UNIV_I, rtac sym, rtac o_apply];
   in
     EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
@@ -201,7 +201,7 @@
       (fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) =>
         EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
           if m = 0 then K all_tac
-          else EVERY' [rtac Un_cong, rtac box_equals,
+          else EVERY' [rtac Un_cong, rtac @{thm box_equals},
             rtac (nth passive_set_map0s (j - 1) RS sym),
             rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
@@ -637,7 +637,7 @@
         ks to_sbd_injs from_to_sbds)];
   in
     (rtac mor_cong THEN'
-    EVERY' (map (fn thm => rtac (thm RS ext)) beh_defs) THEN'
+    EVERY' (map (fn thm => rtac (thm RS @{thm ext})) beh_defs) THEN'
     stac mor_def THEN' rtac conjI THEN'
     CONJ_WRAP' fbetw_tac
       (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~
@@ -702,7 +702,7 @@
 fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
   EVERY' [rtac iffD2, rtac mor_UNIV,
     CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
-      EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
+      EVERY' [rtac @{thm ext}, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
         rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
         rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
         rtac (o_apply RS trans RS sym), rtac map_cong0,
@@ -737,12 +737,12 @@
 
 fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
   CONJ_WRAP' (fn (raw_coind, unfold_def) =>
-    EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
+    EVERY' [rtac @{thm ext}, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
       rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
       rtac (o_apply RS sym), rtac 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 ext, rtac trans, rtac o_apply,
+  unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply,
     rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
     EVERY' (map (fn thm =>
       rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
@@ -774,8 +774,9 @@
       rtac CollectI, etac @{thm case_prodI}])) rel_congs] 1;
 
 fun mk_map_tac m n map_arg_cong unfold map_comp map_cong0 =
-  EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
-    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0,
+  EVERY' [rtac @{thm ext}, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
+    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS @{thm box_equals})),
+    rtac map_cong0,
     REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
     REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
     rtac map_arg_cong, rtac (o_apply RS sym)] 1;
@@ -875,9 +876,9 @@
   end;
 
 fun mk_set_map0_tac hset_def col_natural =
-  EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym,
-    (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans),
-    (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1;
+  EVERY' (map rtac [@{thm ext}, o_apply RS trans, hset_def RS trans, sym,
+    o_apply RS trans, @{thm image_cong} OF [hset_def, refl] RS trans,
+    @{thm image_UN} RS trans, refl RS @{thm UN_cong}, col_natural]) 1;
 
 fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
   let
@@ -965,7 +966,7 @@
         rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
         CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
           EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
-            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map0,
+            rtac ord_eq_le_trans, rtac @{thm box_equals}, rtac passive_set_map0,
             rtac (dtor_ctor 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_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
@@ -985,7 +986,7 @@
         (dtor_sets ~~ passive_set_map0s),
         rtac conjI,
         REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
-          rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
+          rtac @{thm box_equals}, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
           rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
           EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]},
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -174,7 +174,7 @@
 fun mk_mor_UNIV_tac m morEs mor_def =
   let
     val n = length morEs;
-    fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
+    fun mor_tac morE = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, etac morE,
       rtac CollectI, CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto m + n),
       rtac sym, rtac o_apply];
   in
@@ -507,7 +507,7 @@
   end;
 
 fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
-  EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx,
+  EVERY' [stac dtor_def, rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx,
     rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
     EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
       ctor_o_folds),
@@ -568,7 +568,8 @@
   end;
 
 fun mk_map_tac m n foldx map_comp_id map_cong0 =
-  EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, rtac o_apply,
+  EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans,
+    rtac o_apply,
     rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong0 RS arg_cong),
     REPEAT_DETERM_N m o rtac refl,
     REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
@@ -579,7 +580,7 @@
   unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
   ALLGOALS atac;
 
-fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
+fun mk_set_tac foldx = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply,
   rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
 
 fun mk_ctor_set_tac set set_map set_maps =
@@ -674,7 +675,7 @@
     val map_comp0s' = drop i map_comp0s @ take i map_comp0s;
     val ctor_maps' = drop i ctor_maps @ take i ctor_maps;
     fun mk_comp comp simp =
-      EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
+      EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
         rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp,
         rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply];
   in
@@ -682,7 +683,7 @@
   end;
 
 fun mk_set_map0_tac set_nat =
-  EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
+  EVERY' (map rtac [@{thm ext}, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
 
 fun mk_bd_card_order_tac bd_card_orders =
   CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders 1;
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/BNF/bnf_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -47,7 +47,7 @@
   |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
   |> mk_Trueprop_eq
   |> (fn goal => Goal.prove_sorry ctxt [] [] goal
-    (K (rtac ext 1 THEN unfold_thms_tac ctxt [o_apply, mk_sym thm] THEN rtac refl 1)))
+    (K (rtac @{thm ext} 1 THEN unfold_thms_tac ctxt [o_apply, mk_sym thm] THEN rtac refl 1)))
   |> Thm.close_derivation;
 
 
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -382,7 +382,7 @@
                    (map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
                  HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts
                    (r $ (a $ Datatype_Aux.app_bnds f i)), f))))
-              (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
+              (fn _ => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1),
                  REPEAT (etac allE 1), rtac thm 1, atac 1])
           end
       in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
@@ -432,7 +432,7 @@
                           map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
                         REPEAT (cong_tac 1), rtac refl 1,
                         REPEAT (atac 1 ORELSE (EVERY
-                          [REPEAT (rtac ext 1),
+                          [REPEAT (rtac @{thm ext} 1),
                            REPEAT (eresolve_tac (mp :: allE ::
                              map make_elim (Suml_inject :: Sumr_inject ::
                                Lim_inject :: inj_thms') @ fun_congs) 1),
@@ -487,7 +487,7 @@
                 Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
               rewrite_goals_tac ctxt (map Thm.symmetric range_eqs),
               REPEAT (EVERY
-                [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
+                [REPEAT (eresolve_tac ([rangeE, @{thm ex1_implies_ex} RS exE] @
                    maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
                  TRY (hyp_subst_tac ctxt 1),
                  rtac (sym RS range_eqI) 1,
@@ -559,10 +559,10 @@
           (fn {context = ctxt, ...} => EVERY
             [rtac iffI 1,
              REPEAT (etac conjE 2), hyp_subst_tac ctxt 2, rtac refl 2,
-             dresolve_tac rep_congs 1, dtac box_equals 1,
+             dresolve_tac rep_congs 1, dtac @{thm box_equals} 1,
              REPEAT (resolve_tac rep_thms 1),
              REPEAT (eresolve_tac inj_thms 1),
-             REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
+             REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac @{thm ext} 1),
                REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
                atac 1]))])
       end;
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -172,7 +172,7 @@
           in
             (EVERY
               [DETERM tac,
-                REPEAT (etac ex1E 1), rtac ex1I 1,
+                REPEAT (etac @{thm ex1E} 1), rtac @{thm ex1I} 1,
                 DEPTH_SOLVE_1 (ares_tac [intr] 1),
                 REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
                 etac elim 1,
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -366,7 +366,7 @@
     val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
 
     val exactly_one =
-      ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
+      @{thm ex1I} |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
       |> curry (op COMP) existence
       |> curry (op COMP) uniqueness
       |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -707,7 +707,7 @@
 fun MESON preskolem_tac mkcl cltac ctxt i st =
   SELECT_GOAL
     (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
-            rtac ccontr 1,
+            rtac @{thm ccontr} 1,
             preskolem_tac,
             Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
                       EVERY1 [skolemize_prems_tac ctxt negs,
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -106,7 +106,7 @@
               SOME (close (Goal.prove ctxt [] [])
                 (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
                 (K (EVERY
-                  [rtac eq_reflection 1, REPEAT (rtac ext 1), rtac iffI 1,
+                  [rtac eq_reflection 1, REPEAT (rtac @{thm ext} 1), rtac iffI 1,
                    EVERY [etac conjE 1, rtac IntI 1, simp, simp,
                      etac IntE 1, rtac conjI 1, simp, simp] ORELSE
                    EVERY [etac disjE 1, rtac UnI1 1, simp, rtac UnI2 1, simp,
@@ -527,7 +527,7 @@
                fold_rev (Term.abs o pair "x") Ts
                 (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
                   list_comb (c, params))))))
-            (K (REPEAT (rtac ext 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps
+            (K (REPEAT (rtac @{thm ext} 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps
               [def, mem_Collect_eq, @{thm split_conv}]) 1))
         in
           lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -33,7 +33,7 @@
 structure LA_Logic: LIN_ARITH_LOGIC =
 struct
 
-val ccontr = ccontr;
+val ccontr = @{thm ccontr};
 val conjI = conjI;
 val notI = notI;
 val sym = sym;
@@ -733,7 +733,7 @@
     EVERY' [
       REPEAT_DETERM o etac rev_mp,
       cond_split_tac,
-      rtac ccontr,
+      rtac @{thm ccontr},
       prem_nnf_tac ctxt,
       TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
     ]
diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/sat.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -419,7 +419,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun pre_cnf_tac ctxt =
-  rtac ccontr THEN'
+  rtac @{thm ccontr} THEN'
   Object_Logic.atomize_prems_tac ctxt THEN'
   CONVERSION Drule.beta_eta_conversion;