# HG changeset patch
# User blanchet
# Date 1459159547 -7200
# Node ID d229f9749507f01cdcab91248727d8a3d7ac6eca
# Parent  5b2a7caa855b6c0354235619ce897653d2122b34
tuning

diff -r 5b2a7caa855b -r d229f9749507 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- 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;
diff -r 5b2a7caa855b -r d229f9749507 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- 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
diff -r 5b2a7caa855b -r d229f9749507 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML
--- 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)))
diff -r 5b2a7caa855b -r d229f9749507 src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML
--- 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) ::