# HG changeset patch # User blanchet # Date 1500501376 -3600 # Node ID e5995950b98ae220d401e3dde1dff663eccab030 # Parent 005a30862ed0029232fb0240048adf2960bcc33e strengthened tactic (for 'fun' BNF) diff -r 005a30862ed0 -r e5995950b98a src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- 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 =