# 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;