# HG changeset patch
# User traytel
# Date 1410162726 -7200
# Node ID 9003cc8ac94d6361ac9bdb04d4350397247594d2
# Parent  be1d10595b7b572eccb2594bc486648549d7427a
made tactic more robust w.r.t. dead variables

diff -r be1d10595b7b -r 9003cc8ac94d src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Sun Sep 07 17:51:32 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Sep 08 09:52:06 2014 +0200
@@ -182,12 +182,14 @@
     val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs;
     val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs;
 
+    val rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
+
     val rel_xtor_co_induct_thm =
-      mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys xtors
-        xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos)
+      mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
+        xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
+          rel_monos rel_eqs)
         lthy;
 
-    val rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
     val map_id0s = no_refl (map map_id0_of_bnf bnfs);
 
     val xtor_co_induct_thm =
diff -r be1d10595b7b -r 9003cc8ac94d src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Sun Sep 07 17:51:32 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Mon Sep 08 09:52:06 2014 +0200
@@ -8,7 +8,7 @@
 signature BNF_FP_N2M_TACTICS =
 sig
   val mk_rel_xtor_co_induct_tactic: BNF_Util.fp_kind -> thm list -> thm list -> thm list ->
-    thm list -> {prems: thm list, context: Proof.context} -> tactic
+    thm list -> thm list -> {prems: thm list, context: Proof.context} -> tactic
 end;
 
 structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS =
@@ -20,10 +20,10 @@
 
 val vimage2p_unfolds = o_apply :: @{thms vimage2p_def};
 
-fun mk_rel_xtor_co_induct_tactic fp abs_inverses co_inducts0 rel_defs rel_monos
+fun mk_rel_xtor_co_induct_tactic fp abs_inverses co_inducts0 rel_defs rel_monos nesting_rel_eqs
   {context = ctxt, prems = raw_C_IHs} =
   let
-    val co_inducts = map (unfold_thms ctxt vimage2p_unfolds) co_inducts0;
+    val co_inducts = map (unfold_thms ctxt (vimage2p_unfolds @ nesting_rel_eqs)) co_inducts0;
     val unfolds = map (fn def =>
       unfold_thms ctxt (id_apply :: vimage2p_unfolds @ abs_inverses @ no_reflexive [def])) rel_defs;
     val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;