# HG changeset patch
# User traytel
# Date 1459451985 -7200
# Node ID f0e8ed202ce5fda906aaf48994c223a4c873e390
# Parent  596baa1a32517e7749b3192e4b94362d356c3edc
made tactic more robust

diff -r 596baa1a3251 -r f0e8ed202ce5 src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Thu Mar 31 08:38:50 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Thu Mar 31 21:19:45 2016 +0200
@@ -38,6 +38,8 @@
         |> op RS
         |> unfold)
       folded_C_IHs rel_monos unfolds;
+
+    val sym_nested_rel_eqs = map mk_sym nesting_rel_eqs;
   in
     unfold_thms_tac ctxt vimage2p_unfolds THEN
     HEADGOAL (CONJ_WRAP_GEN' (rtac ctxt @{thm context_conjI})
@@ -45,7 +47,10 @@
          REPEAT_ALL_NEW (FIRST' [eresolve_tac ctxt C_IHs, eresolve_tac ctxt C_IH_monos,
            SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac ctxt @{thm order_refl},
            assume_tac ctxt, resolve_tac ctxt co_inducts,
-           resolve_tac ctxt C_IH_monos THEN' REPEAT_ALL_NEW (eresolve_tac ctxt nesting_rel_monos)])))
+           resolve_tac ctxt C_IH_monos THEN_ALL_NEW (TRY o FIRST'
+             [SELECT_GOAL (unfold_thms_tac ctxt sym_nested_rel_eqs) THEN' assume_tac ctxt,
+              rtac ctxt @{thm order_refl},
+              REPEAT_ALL_NEW (eresolve_tac ctxt nesting_rel_monos)])])))
     co_inducts)
   end;