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