# HG changeset patch
# User desharna
# Date 1682607963 -7200
# Node ID 1249dadc95066e187abb424d9dbe5b4a5729aedb
# Parent  8734ca279e59a524fa244bbc4f7fed0f4a4ca10f# Parent  64beebac04b8f0eb2d78ad004def53955a21e85e
merged

diff -r 8734ca279e59 -r 1249dadc9506 NEWS
--- a/NEWS	Thu Apr 27 11:50:14 2023 +0200
+++ b/NEWS	Thu Apr 27 17:06:03 2023 +0200
@@ -257,6 +257,9 @@
       totalp_on_multpDM
       totalp_on_multpHO
 
+* 'primcorec': Made the internal tactic more robust in the face of
+  nested corecursion.
+
 * HOL-Algebra: new theories SimpleGroups (simple groups) 
   and SndIsomorphismGrp (second isomorphism theorem for groups), 
   by Jakob von Raumer
diff -r 8734ca279e59 -r 1249dadc9506 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Apr 27 11:50:14 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Apr 27 17:06:03 2023 +0200
@@ -141,6 +141,9 @@
     etac ctxt notE THEN' assume_tac ctxt 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'
+    (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]]} @
        mapsx @ map_ident0s @ map_comps))) ORELSE'
     fo_rtac ctxt @{thm cong} ORELSE'
     rtac ctxt @{thm ext} ORELSE'