# HG changeset patch
# User traytel
# Date 1707895884 -3600
# Node ID 1b3770369ee7b3c2c38d07aeac6988be16963fea
# Parent  3e27ab965a36941f6911a10886e7ff8068680e60# Parent  f933e915362456c2b377162e89439b8e568fac7b
merged

diff -r f933e9153624 -r 1b3770369ee7 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Feb 13 16:03:55 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed Feb 14 08:31:24 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'