# HG changeset patch
# User traytel
# Date 1410201772 -7200
# Node ID 17200800a5538d6885524834c72a1f2e8e57628f
# Parent  4967e67cc53dd8bf0dc3df03ffdbc9e43900f51b
made tactic even more robust w.r.t. dead variables

diff -r 4967e67cc53d -r 17200800a553 src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Mon Sep 08 19:21:19 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Mon Sep 08 20:42:52 2014 +0200
@@ -23,7 +23,8 @@
 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 @ nesting_rel_eqs)) co_inducts0;
+    val co_inducts = map (unfold_thms ctxt
+      (vimage2p_unfolds @ @{thms prod.rel_eq sum.rel_eq} @ 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;