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