more antiquotations;
authorwenzelm
Fri Mar 07 22:30:58 2014 +0100 (2014-03-07)
changeset 5599041c6b99c5fb7
parent 55989 55827fc7c0dd
child 55991 3fa6e6c81788
more antiquotations;
src/HOL/Fun.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Tools/BNF/bnf_comp_tactics.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_tactics.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/sat.ML
     1.1 --- a/src/HOL/Fun.thy	Fri Mar 07 22:19:52 2014 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Mar 07 22:30:58 2014 +0100
     1.3 @@ -895,7 +895,7 @@
     1.4            SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
     1.5              (fn _ =>
     1.6                rtac eq_reflection 1 THEN
     1.7 -              rtac ext 1 THEN
     1.8 +              rtac @{thm ext} 1 THEN
     1.9                simp_tac (put_simpset ss ctxt) 1))
    1.10      end
    1.11  in proc end
     2.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 07 22:19:52 2014 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Mar 07 22:30:58 2014 +0100
     2.3 @@ -1723,8 +1723,8 @@
     2.4                  (finite_thss ~~ finite_ctxt_ths) @
     2.5              maps (fn ((_, idxss), elim) => maps (fn idxs =>
     2.6                [full_simp_tac (put_simpset HOL_ss context addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1,
     2.7 -               REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
     2.8 -               rtac ex1I 1,
     2.9 +               REPEAT_DETERM (eresolve_tac @{thms conjE ex1E} 1),
    2.10 +               rtac @{thm ex1I} 1,
    2.11                 (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
    2.12                 rotate_tac ~1 1,
    2.13                 ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
     3.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Fri Mar 07 22:19:52 2014 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Mar 07 22:30:58 2014 +0100
     3.3 @@ -241,7 +241,7 @@
     3.4  (* applies the ext-rule such that      *)
     3.5  (*                                     *)
     3.6  (*    f = g   goes to  /\x. f x = g x  *)
     3.7 -fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
     3.8 +fun ext_fun_tac i = ("extensionality expansion of functions", rtac @{thm ext} i);
     3.9  
    3.10  
    3.11  (* perm_extend_simp_tac_i is perm_simp plus additional tactics        *)
     4.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
     4.3 @@ -55,17 +55,17 @@
     4.4    rtac refl 1;
     4.5  
     4.6  fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s =
     4.7 -  EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
     4.8 +  EVERY' ([rtac @{thm ext}, rtac (Gmap_cong0 RS trans)] @
     4.9      map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1;
    4.10  
    4.11  fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s =
    4.12 -  EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
    4.13 +  EVERY' ([rtac @{thm ext}, rtac sym, rtac trans_o_apply,
    4.14      rtac (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), rtac Gmap_cong0] @
    4.15      map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1;
    4.16  
    4.17  fun mk_comp_set_map0_tac ctxt set'_eq_set Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
    4.18    unfold_thms_tac ctxt [set'_eq_set] THEN
    4.19 -  EVERY' ([rtac ext] @
    4.20 +  EVERY' ([rtac @{thm ext}] @
    4.21      replicate 3 (rtac trans_o_apply) @
    4.22      [rtac (arg_cong_Union RS trans),
    4.23       rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
    4.24 @@ -79,7 +79,7 @@
    4.25       rtac @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]},
    4.26       rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
    4.27       [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]},
    4.28 -        rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
    4.29 +        rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac @{thm ext}, rtac trans_o_apply,
    4.30          rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]},
    4.31          rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
    4.32       rtac @{thm image_empty}]) 1;
     5.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
     5.3 @@ -84,7 +84,8 @@
     5.4          hyp_subst_tac ctxt,
     5.5          rtac @{thm relcomppI}, rtac @{thm conversepI},
     5.6          EVERY' (map2 (fn convol => fn map_id0 =>
     5.7 -          EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]),
     5.8 +          EVERY' [rtac @{thm GrpI},
     5.9 +            rtac (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_id0]),
    5.10              REPEAT_DETERM_N n o rtac (convol RS fun_cong),
    5.11              REPEAT_DETERM o eresolve_tac [CollectE, conjE],
    5.12              rtac CollectI,
    5.13 @@ -203,7 +204,7 @@
    5.14        rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, in_tac,
    5.15        rtac conjI,
    5.16        EVERY' (map (fn convol =>
    5.17 -        rtac (box_equals OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
    5.18 +        rtac (@{thm box_equals} OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
    5.19          REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})])
    5.20    end;
    5.21  
    5.22 @@ -254,7 +255,7 @@
    5.23            (K (etac @{thm If_the_inv_into_in_Func} THEN' atac)) set_maps,
    5.24          rtac sym,
    5.25          rtac (Drule.rotate_prems 1
    5.26 -           ((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
    5.27 +           ((@{thm box_equals} OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
    5.28               map_comp RS sym, map_id]) RSN (2, trans))),
    5.29          REPEAT_DETERM_N (2 * live) o atac,
    5.30          REPEAT_DETERM_N live o rtac (@{thm prod.case} RS trans),
    5.31 @@ -265,7 +266,7 @@
    5.32            rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]})
    5.33          set_maps,
    5.34          rtac sym,
    5.35 -        rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
    5.36 +        rtac (@{thm box_equals} OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
    5.37             map_comp RS sym, map_id])] 1
    5.38    end;
    5.39  
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 22:19:52 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 22:30:58 2014 +0100
     6.3 @@ -525,7 +525,8 @@
     6.4      val map_cong_active_args2 = replicate n (if is_rec
     6.5        then case_fp fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id}
     6.6        else case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong);
     6.7 -    fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
     6.8 +    fun mk_map_congs passive active =
     6.9 +      map (fn thm => thm OF (passive @ active) RS @{thm ext}) map_cong0s;
    6.10      val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
    6.11      val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;
    6.12      
     7.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
     7.3 @@ -140,7 +140,7 @@
     7.4      (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
     7.5         sum.case} @ mapsx @ map_comps @ map_idents))) ORELSE'
     7.6      fo_rtac @{thm cong} ctxt ORELSE'
     7.7 -    rtac ext));
     7.8 +    rtac @{thm ext}));
     7.9  
    7.10  fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
    7.11    HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
     8.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
     8.3 @@ -145,7 +145,7 @@
     8.4  fun mk_mor_UNIV_tac morEs mor_def =
     8.5    let
     8.6      val n = length morEs;
     8.7 -    fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
     8.8 +    fun mor_tac morE = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, etac morE,
     8.9        rtac UNIV_I, rtac sym, rtac o_apply];
    8.10    in
    8.11      EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
    8.12 @@ -201,7 +201,7 @@
    8.13        (fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) =>
    8.14          EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
    8.15            if m = 0 then K all_tac
    8.16 -          else EVERY' [rtac Un_cong, rtac box_equals,
    8.17 +          else EVERY' [rtac Un_cong, rtac @{thm box_equals},
    8.18              rtac (nth passive_set_map0s (j - 1) RS sym),
    8.19              rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
    8.20            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
    8.21 @@ -637,7 +637,7 @@
    8.22          ks to_sbd_injs from_to_sbds)];
    8.23    in
    8.24      (rtac mor_cong THEN'
    8.25 -    EVERY' (map (fn thm => rtac (thm RS ext)) beh_defs) THEN'
    8.26 +    EVERY' (map (fn thm => rtac (thm RS @{thm ext})) beh_defs) THEN'
    8.27      stac mor_def THEN' rtac conjI THEN'
    8.28      CONJ_WRAP' fbetw_tac
    8.29        (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~
    8.30 @@ -702,7 +702,7 @@
    8.31  fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
    8.32    EVERY' [rtac iffD2, rtac mor_UNIV,
    8.33      CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
    8.34 -      EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
    8.35 +      EVERY' [rtac @{thm ext}, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
    8.36          rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
    8.37          rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
    8.38          rtac (o_apply RS trans RS sym), rtac map_cong0,
    8.39 @@ -737,12 +737,12 @@
    8.40  
    8.41  fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
    8.42    CONJ_WRAP' (fn (raw_coind, unfold_def) =>
    8.43 -    EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
    8.44 +    EVERY' [rtac @{thm ext}, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
    8.45        rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
    8.46        rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
    8.47  
    8.48  fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors =
    8.49 -  unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
    8.50 +  unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply,
    8.51      rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
    8.52      EVERY' (map (fn thm =>
    8.53        rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
    8.54 @@ -774,8 +774,9 @@
    8.55        rtac CollectI, etac @{thm case_prodI}])) rel_congs] 1;
    8.56  
    8.57  fun mk_map_tac m n map_arg_cong unfold map_comp map_cong0 =
    8.58 -  EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
    8.59 -    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0,
    8.60 +  EVERY' [rtac @{thm ext}, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
    8.61 +    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS @{thm box_equals})),
    8.62 +    rtac map_cong0,
    8.63      REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
    8.64      REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
    8.65      rtac map_arg_cong, rtac (o_apply RS sym)] 1;
    8.66 @@ -875,9 +876,9 @@
    8.67    end;
    8.68  
    8.69  fun mk_set_map0_tac hset_def col_natural =
    8.70 -  EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym,
    8.71 -    (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans),
    8.72 -    (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1;
    8.73 +  EVERY' (map rtac [@{thm ext}, o_apply RS trans, hset_def RS trans, sym,
    8.74 +    o_apply RS trans, @{thm image_cong} OF [hset_def, refl] RS trans,
    8.75 +    @{thm image_UN} RS trans, refl RS @{thm UN_cong}, col_natural]) 1;
    8.76  
    8.77  fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
    8.78    let
    8.79 @@ -965,7 +966,7 @@
    8.80          rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
    8.81          CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
    8.82            EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
    8.83 -            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map0,
    8.84 +            rtac ord_eq_le_trans, rtac @{thm box_equals}, rtac passive_set_map0,
    8.85              rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
    8.86              CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
    8.87                (fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
    8.88 @@ -985,7 +986,7 @@
    8.89          (dtor_sets ~~ passive_set_map0s),
    8.90          rtac conjI,
    8.91          REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
    8.92 -          rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
    8.93 +          rtac @{thm box_equals}, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
    8.94            rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
    8.95            EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
    8.96              dtac @{thm ssubst_mem[OF pair_collapse]},
     9.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
     9.3 @@ -174,7 +174,7 @@
     9.4  fun mk_mor_UNIV_tac m morEs mor_def =
     9.5    let
     9.6      val n = length morEs;
     9.7 -    fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE,
     9.8 +    fun mor_tac morE = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, etac morE,
     9.9        rtac CollectI, CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto m + n),
    9.10        rtac sym, rtac o_apply];
    9.11    in
    9.12 @@ -507,7 +507,7 @@
    9.13    end;
    9.14  
    9.15  fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
    9.16 -  EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx,
    9.17 +  EVERY' [stac dtor_def, rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx,
    9.18      rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
    9.19      EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
    9.20        ctor_o_folds),
    9.21 @@ -568,7 +568,8 @@
    9.22    end;
    9.23  
    9.24  fun mk_map_tac m n foldx map_comp_id map_cong0 =
    9.25 -  EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, rtac o_apply,
    9.26 +  EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans,
    9.27 +    rtac o_apply,
    9.28      rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong0 RS arg_cong),
    9.29      REPEAT_DETERM_N m o rtac refl,
    9.30      REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
    9.31 @@ -579,7 +580,7 @@
    9.32    unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
    9.33    ALLGOALS atac;
    9.34  
    9.35 -fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
    9.36 +fun mk_set_tac foldx = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply,
    9.37    rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
    9.38  
    9.39  fun mk_ctor_set_tac set set_map set_maps =
    9.40 @@ -674,7 +675,7 @@
    9.41      val map_comp0s' = drop i map_comp0s @ take i map_comp0s;
    9.42      val ctor_maps' = drop i ctor_maps @ take i ctor_maps;
    9.43      fun mk_comp comp simp =
    9.44 -      EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
    9.45 +      EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
    9.46          rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp,
    9.47          rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply];
    9.48    in
    9.49 @@ -682,7 +683,7 @@
    9.50    end;
    9.51  
    9.52  fun mk_set_map0_tac set_nat =
    9.53 -  EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
    9.54 +  EVERY' (map rtac [@{thm ext}, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
    9.55  
    9.56  fun mk_bd_card_order_tac bd_card_orders =
    9.57    CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders 1;
    10.1 --- a/src/HOL/Tools/BNF/bnf_tactics.ML	Fri Mar 07 22:19:52 2014 +0100
    10.2 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Fri Mar 07 22:30:58 2014 +0100
    10.3 @@ -47,7 +47,7 @@
    10.4    |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
    10.5    |> mk_Trueprop_eq
    10.6    |> (fn goal => Goal.prove_sorry ctxt [] [] goal
    10.7 -    (K (rtac ext 1 THEN unfold_thms_tac ctxt [o_apply, mk_sym thm] THEN rtac refl 1)))
    10.8 +    (K (rtac @{thm ext} 1 THEN unfold_thms_tac ctxt [o_apply, mk_sym thm] THEN rtac refl 1)))
    10.9    |> Thm.close_derivation;
   10.10  
   10.11  
    11.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 07 22:19:52 2014 +0100
    11.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 07 22:30:58 2014 +0100
    11.3 @@ -382,7 +382,7 @@
    11.4                     (map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
    11.5                   HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts
    11.6                     (r $ (a $ Datatype_Aux.app_bnds f i)), f))))
    11.7 -              (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
    11.8 +              (fn _ => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1),
    11.9                   REPEAT (etac allE 1), rtac thm 1, atac 1])
   11.10            end
   11.11        in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
   11.12 @@ -432,7 +432,7 @@
   11.13                            map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
   11.14                          REPEAT (cong_tac 1), rtac refl 1,
   11.15                          REPEAT (atac 1 ORELSE (EVERY
   11.16 -                          [REPEAT (rtac ext 1),
   11.17 +                          [REPEAT (rtac @{thm ext} 1),
   11.18                             REPEAT (eresolve_tac (mp :: allE ::
   11.19                               map make_elim (Suml_inject :: Sumr_inject ::
   11.20                                 Lim_inject :: inj_thms') @ fun_congs) 1),
   11.21 @@ -487,7 +487,7 @@
   11.22                  Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
   11.23                rewrite_goals_tac ctxt (map Thm.symmetric range_eqs),
   11.24                REPEAT (EVERY
   11.25 -                [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
   11.26 +                [REPEAT (eresolve_tac ([rangeE, @{thm ex1_implies_ex} RS exE] @
   11.27                     maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
   11.28                   TRY (hyp_subst_tac ctxt 1),
   11.29                   rtac (sym RS range_eqI) 1,
   11.30 @@ -559,10 +559,10 @@
   11.31            (fn {context = ctxt, ...} => EVERY
   11.32              [rtac iffI 1,
   11.33               REPEAT (etac conjE 2), hyp_subst_tac ctxt 2, rtac refl 2,
   11.34 -             dresolve_tac rep_congs 1, dtac box_equals 1,
   11.35 +             dresolve_tac rep_congs 1, dtac @{thm box_equals} 1,
   11.36               REPEAT (resolve_tac rep_thms 1),
   11.37               REPEAT (eresolve_tac inj_thms 1),
   11.38 -             REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
   11.39 +             REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac @{thm ext} 1),
   11.40                 REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
   11.41                 atac 1]))])
   11.42        end;
    12.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 07 22:19:52 2014 +0100
    12.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 07 22:30:58 2014 +0100
    12.3 @@ -172,7 +172,7 @@
    12.4            in
    12.5              (EVERY
    12.6                [DETERM tac,
    12.7 -                REPEAT (etac ex1E 1), rtac ex1I 1,
    12.8 +                REPEAT (etac @{thm ex1E} 1), rtac @{thm ex1I} 1,
    12.9                  DEPTH_SOLVE_1 (ares_tac [intr] 1),
   12.10                  REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
   12.11                  etac elim 1,
    13.1 --- a/src/HOL/Tools/Function/function_core.ML	Fri Mar 07 22:19:52 2014 +0100
    13.2 +++ b/src/HOL/Tools/Function/function_core.ML	Fri Mar 07 22:30:58 2014 +0100
    13.3 @@ -366,7 +366,7 @@
    13.4      val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
    13.5  
    13.6      val exactly_one =
    13.7 -      ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
    13.8 +      @{thm ex1I} |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
    13.9        |> curry (op COMP) existence
   13.10        |> curry (op COMP) uniqueness
   13.11        |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
    14.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 07 22:19:52 2014 +0100
    14.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 07 22:30:58 2014 +0100
    14.3 @@ -707,7 +707,7 @@
    14.4  fun MESON preskolem_tac mkcl cltac ctxt i st =
    14.5    SELECT_GOAL
    14.6      (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
    14.7 -            rtac ccontr 1,
    14.8 +            rtac @{thm ccontr} 1,
    14.9              preskolem_tac,
   14.10              Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
   14.11                        EVERY1 [skolemize_prems_tac ctxt negs,
    15.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Mar 07 22:19:52 2014 +0100
    15.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Mar 07 22:30:58 2014 +0100
    15.3 @@ -106,7 +106,7 @@
    15.4                SOME (close (Goal.prove ctxt [] [])
    15.5                  (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
    15.6                  (K (EVERY
    15.7 -                  [rtac eq_reflection 1, REPEAT (rtac ext 1), rtac iffI 1,
    15.8 +                  [rtac eq_reflection 1, REPEAT (rtac @{thm ext} 1), rtac iffI 1,
    15.9                     EVERY [etac conjE 1, rtac IntI 1, simp, simp,
   15.10                       etac IntE 1, rtac conjI 1, simp, simp] ORELSE
   15.11                     EVERY [etac disjE 1, rtac UnI1 1, simp, rtac UnI2 1, simp,
   15.12 @@ -527,7 +527,7 @@
   15.13                 fold_rev (Term.abs o pair "x") Ts
   15.14                  (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
   15.15                    list_comb (c, params))))))
   15.16 -            (K (REPEAT (rtac ext 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps
   15.17 +            (K (REPEAT (rtac @{thm ext} 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps
   15.18                [def, mem_Collect_eq, @{thm split_conv}]) 1))
   15.19          in
   15.20            lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    16.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Mar 07 22:19:52 2014 +0100
    16.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Mar 07 22:30:58 2014 +0100
    16.3 @@ -33,7 +33,7 @@
    16.4  structure LA_Logic: LIN_ARITH_LOGIC =
    16.5  struct
    16.6  
    16.7 -val ccontr = ccontr;
    16.8 +val ccontr = @{thm ccontr};
    16.9  val conjI = conjI;
   16.10  val notI = notI;
   16.11  val sym = sym;
   16.12 @@ -733,7 +733,7 @@
   16.13      EVERY' [
   16.14        REPEAT_DETERM o etac rev_mp,
   16.15        cond_split_tac,
   16.16 -      rtac ccontr,
   16.17 +      rtac @{thm ccontr},
   16.18        prem_nnf_tac ctxt,
   16.19        TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
   16.20      ]
    17.1 --- a/src/HOL/Tools/sat.ML	Fri Mar 07 22:19:52 2014 +0100
    17.2 +++ b/src/HOL/Tools/sat.ML	Fri Mar 07 22:30:58 2014 +0100
    17.3 @@ -419,7 +419,7 @@
    17.4  (* ------------------------------------------------------------------------- *)
    17.5  
    17.6  fun pre_cnf_tac ctxt =
    17.7 -  rtac ccontr THEN'
    17.8 +  rtac @{thm ccontr} THEN'
    17.9    Object_Logic.atomize_prems_tac ctxt THEN'
   17.10    CONVERSION Drule.beta_eta_conversion;
   17.11