--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Mar 28 12:05:47 2016 +0200
@@ -1161,7 +1161,7 @@
fun derive_eval_thm ctxt dtor_inject dtor_unfold_thm eval_def =
(trans OF [iffD2 OF [dtor_inject, eval_def RS meta_eq_to_obj_eq RS fun_cong], dtor_unfold_thm])
- |> unfold_thms ctxt [o_apply, eval_def RS Drule.symmetric_thm];
+ |> unfold_thms ctxt [o_apply, eval_def RS symmetric_thm];
fun derive_eval_flat ctxt Y Z fpT ssig_T dead_ssig_map flat eval x dead_pre_map_comp0
dtor_unfold_unique ssig_map_id ssig_map_comp flat_pointful_natural eval_core_pointful_natural
@@ -1360,8 +1360,8 @@
in
unfold_thms ctxt @{thms atomize_imp}
(((inject_refine' OF [extdd_o_VLeaf, extdd_o_VLeaf] RS iffD1)
- OF [Drule.asm_rl, corecU_pointfree])
- OF [Drule.asm_rl, trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]
+ OF [asm_rl, corecU_pointfree])
+ OF [asm_rl, trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]
OF [extdd_mor, corecU_pointfree RS extdd_mor]])
RS @{thm obj_distinct_prems}
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Mar 28 12:05:47 2016 +0200
@@ -273,7 +273,7 @@
val var = Free (var_name, fpT);
val goal = mk_Trueprop_eq (expand_to_ctr_term ctxt fpT var, var);
- val exhaust' = Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt var)] exhaust;
+ val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt var)] exhaust;
in
Goal.prove_sorry ctxt [var_name] [] goal (fn {context = ctxt, prems = _} =>
HEADGOAL (rtac ctxt exhaust') THEN ALLGOALS (hyp_subst_tac ctxt) THEN
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Mon Mar 28 12:05:47 2016 +0200
@@ -47,15 +47,13 @@
end;
fun instantiate_distrib thm ctxt t =
- Drule.infer_instantiate' ctxt [SOME (Thm.incr_indexes_cterm 1 (Thm.cterm_of ctxt t))] thm;
+ infer_instantiate' ctxt [SOME (Thm.incr_indexes_cterm 1 (Thm.cterm_of ctxt t))] thm;
-(* TODO (here and elsewhere): Use metaequality in goal instead and keep uninstianted version of
- theorem? *)
val mk_if_distrib_of = instantiate_distrib @{thm if_distrib};
val mk_case_sum_distrib_of = instantiate_distrib @{thm sum.case_distrib};
fun mk_case_dtor_tac ctxt u abs_inverse dtor_ctor ctr_defs exhaust cases =
- let val exhaust' = Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in
+ let val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in
HEADGOAL (rtac ctxt exhaust') THEN
REPEAT_DETERM (HEADGOAL (etac ctxt ssubst THEN'
SELECT_GOAL (unfold_thms_tac ctxt cases THEN
@@ -180,7 +178,7 @@
end;
fun mk_last_disc_tac ctxt u exhaust discs' =
- let val exhaust' = Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in
+ let val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in
HEADGOAL (rtac ctxt exhaust') THEN
REPEAT_DETERM (HEADGOAL (etac ctxt ssubst THEN'
simp_tac (ss_only (distinct Thm.eq_thm discs' @ @{thms simp_thms}) ctxt)))
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML Mon Mar 28 12:05:47 2016 +0200
@@ -163,7 +163,7 @@
sctr_pointful_natural eval_sctr_pointful corecUU_def =
unfold_thms_tac ctxt [corecUU_def] THEN
HEADGOAL (rtac ctxt ext THEN' subst_tac ctxt NONE [corecU_ctor RS sym]) THEN
- unfold_thms_tac ctxt [corecUU_def RS Drule.symmetric_thm] THEN
+ unfold_thms_tac ctxt [corecUU_def RS symmetric_thm] THEN
HEADGOAL (rtac ctxt (dtor_inject RS iffD1) THEN'
mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp
flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural
@@ -241,7 +241,7 @@
old_eval eval =
HEADGOAL (rtac ctxt (unfold_thms ctxt [o_apply]
(trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] OF [ext, ext])
- OF [Drule.asm_rl, old_eval RS sym])) THEN
+ OF [asm_rl, old_eval RS sym])) THEN
unfold_thms_tac ctxt [dead_pre_map_comp0, embL_pointful_natural, eval_core_embL, eval,
o_apply] THEN
HEADGOAL (rtac ctxt refl);
@@ -359,7 +359,7 @@
asm_simp_tac (ss_only_silent ((mk_pointful ctxt prem RS sym) :: dead_pre_map_comp0 ::
cutSsig_def_pointful_natural :: flat_simps @
@{thms o_apply convol_apply map_prod_simp id_apply}) ctxt) THEN'
- rtac ctxt (dead_pre_map_cong OF [Drule.asm_rl, refl]) THEN'
+ rtac ctxt (dead_pre_map_cong OF [asm_rl, refl]) THEN'
asm_simp_tac (ss_only_silent (ssig_map_comp :: cutSsig_def :: flat_pointful_natural ::
eval_core_flat :: unfold_thms ctxt [o_def] dead_pre_map_comp :: (dead_ssig_map_comp0 RS sym) ::
(flat_flat RS sym) ::