--- 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'