# HG changeset patch
# User blanchet
# Date 1682604919 -7200
# Node ID 64beebac04b8f0eb2d78ad004def53955a21e85e
# Parent  5aae99b191ebdc6741bddd8dae30e17f573c3761
made 'primcorec' more robust

diff -r 5aae99b191eb -r 64beebac04b8 NEWS
--- a/NEWS	Wed Apr 26 22:02:59 2023 +0200
+++ b/NEWS	Thu Apr 27 16:15:19 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 5aae99b191eb -r 64beebac04b8 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed Apr 26 22:02:59 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Apr 27 16:15:19 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'