# HG changeset patch # User traytel # Date 1707831069 -3600 # Node ID 3e27ab965a36941f6911a10886e7ff8068680e60 # Parent 6e5f40cfa877a01d833742c6eac0d47614be1b0e made destructor-view tactic more robust (by Jan van Brügge) diff -r 6e5f40cfa877 -r 3e27ab965a36 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Feb 13 12:23:12 2024 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Feb 13 14:31:09 2024 +0100 @@ -139,6 +139,8 @@ eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' assume_tac ctxt ORELSE' etac ctxt notE THEN' assume_tac ctxt ORELSE' + (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt ( + map (Local_Defs.unfold0 ctxt @{thms id_def[symmetric]}) map_ident0s @ map_comps))) ORELSE' (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @ map_ident0s @ map_comps))) ORELSE'