merged

--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri Apr 01 22:24:18 2016 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri Apr 01 22:33:31 2016 +0200
@@ -138,6 +138,7 @@
 my $thy_text = join("", @lines);
 my $old_len = length($thy_text);
 $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
+$thy_text =~ s/\b$thy_name\./$new_thy_name./g;
 $thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g;
 die "No 'imports' found" if length($thy_text) == $old_len;
 

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Fri Apr 01 22:24:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Fri Apr 01 22:33:31 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;