--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Jul 19 16:41:26 2017 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Jul 19 22:56:16 2017 +0100
@@ -488,8 +488,10 @@
fp_nesting_pred_maps fun_defs recx =
unfold_thms_tac ctxt fun_defs THEN
HEADGOAL (rtac ctxt (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
- unfold_thms_tac ctxt (nested_simps ctxt @ fp_nesting_map_ident0s @ fp_nesting_map_comps @
- fp_nesting_pred_maps) THEN
+ unfold_thms_tac ctxt (fp_nesting_map_ident0s @ fp_nesting_map_comps @ fp_nesting_pred_maps) THEN
+ REPEAT_DETERM (CHANGED (unfold_thms_tac ctxt (fp_nesting_map_ident0s @ fp_nesting_map_comps @
+ fp_nesting_pred_maps) THEN
+ unfold_thms_tac ctxt (nested_simps ctxt))) THEN
HEADGOAL (rtac ctxt refl);
fun prepare_primrec plugins nonexhaustives transfers fixes specs lthy0 =