# HG changeset patch
# User blanchet
# Date 1410963613 -7200
# Node ID 3782c7b0d1cc604d89444022a606da65b0cb3dd6
# Parent  cdce4471d5906789c40aa4ef4c4c2e8dbcf9e814
avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')

diff -r cdce4471d590 -r 3782c7b0d1cc src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Sep 17 12:09:33 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Wed Sep 17 16:20:13 2014 +0200
@@ -837,7 +837,8 @@
       rtac (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1;
     fun rel_OO_Grp_tac ctxt =
       (rtac (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN'
-       subst_tac ctxt NONE [type_definition RS @{thm vimage2p_relcompp_converse}] THEN'
+       (if has_live_phantoms then subst_tac ctxt NONE else SELECT_GOAL o unfold_thms_tac ctxt)
+         [type_definition RS @{thm vimage2p_relcompp_converse}] THEN'
        SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
          type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
          type_definition RS @{thm vimage2p_relcompp_converse}]) THEN'
diff -r cdce4471d590 -r 3782c7b0d1cc src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Sep 17 12:09:33 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Sep 17 16:20:13 2014 +0200
@@ -68,6 +68,11 @@
 val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set;
 val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc};
 
+fun is_def_looping def =
+  (case Thm.prop_of def of
+    Const (@{const_name Pure.eq}, _) $ lhs $ rhs => Term.exists_subterm (curry (op =) lhs) rhs
+  | _ => false);
+
 fun hhf_concl_conv cv ctxt ct =
   (case Thm.term_of ct of
     Const (@{const_name Pure.all}, _) $ Abs _ =>
@@ -145,7 +150,8 @@
       case_unit_Unity} @ sumprod_thms_map;
 
 fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
-  HEADGOAL (subst_tac ctxt NONE [ctr_def]) THEN
+  HEADGOAL ((if is_def_looping ctr_def then subst_tac ctxt NONE
+    else SELECT_GOAL o unfold_thms_tac ctxt) [ctr_def]) THEN
   unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
     pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
 
@@ -195,7 +201,10 @@
 fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' fp_abs_inverses abs_inverses set_maps
     pre_set_defss =
   let val n = Integer.sum ns in
-    EVERY (map (fn th => HEADGOAL (subst_asm_tac ctxt NONE [th])) ctr_defs) THEN
+    (if exists is_def_looping ctr_defs then
+       EVERY (map (fn def => HEADGOAL (subst_asm_tac ctxt NONE [def])) ctr_defs)
+     else
+       unfold_thms_tac ctxt ctr_defs) THEN
     HEADGOAL (rtac ctor_induct') THEN co_induct_inst_as_projs_tac ctxt 0 THEN
     EVERY (map4 (EVERY oooo map3 o
         mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps)