# HG changeset patch
# User wenzelm
# Date 1728504093 -7200
# Node ID 3e3e7a68cd80ee59d15e00308a774fd94d345c0c
# Parent  e66172629fccdd8485ed7bff1df481baa4303fa8
back to specific nonterminals (amending 52ed95fa4656): otherwise AFP/CakeML won't terminate;

diff -r e66172629fcc -r 3e3e7a68cd80 src/HOL/Library/Datatype_Records.thy
--- a/src/HOL/Library/Datatype_Records.thy	Wed Oct 09 22:00:12 2024 +0200
+++ b/src/HOL/Library/Datatype_Records.thy	Wed Oct 09 22:01:33 2024 +0200
@@ -26,6 +26,15 @@
   \<^item> extensible records are not supported
 \<close>
 
+nonterminal
+  ident and
+  field_type and
+  field_types and
+  field and
+  fields and
+  field_update and
+  field_updates
+
 open_bundle datatype_record_syntax
 begin
 
@@ -38,14 +47,14 @@
   "_datatype_field"         :: "ident => 'a => field"               (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>_ =/ _)\<close>)
   ""                        :: "field => fields"                    (\<open>_\<close>)
   "_datatype_fields"        :: "field => fields => fields"          (\<open>_,/ _\<close>)
-  "_datatype_record"        :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix datatype record type\<close>\<close>\<lparr>_\<rparr>)\<close>)
+  "_datatype_record"        :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix datatype record value\<close>\<close>\<lparr>_\<rparr>)\<close>)
   "_datatype_field_update"  :: "ident => 'a => field_update"        (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>_ :=/ _)\<close>)
   ""                        :: "field_update => field_updates"      (\<open>_\<close>)
   "_datatype_field_updates" :: "field_update => field_updates => field_updates"  (\<open>_,/ _\<close>)
   "_datatype_record_update" :: "'a => field_updates => 'b"          (\<open>(\<open>open_block notation=\<open>mixfix datatype record update\<close>\<close>_/(3\<lparr>_\<rparr>))\<close> [900, 0] 900)
 
 syntax (ASCII)
-  "_datatype_record"        :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix datatype record type\<close>\<close>'(| _ |'))\<close>)
+  "_datatype_record"        :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix datatype record value\<close>\<close>'(| _ |'))\<close>)
   "_datatype_record_update" :: "'a => field_updates => 'b"          (\<open>(\<open>open_block notation=\<open>mixfix datatype record update\<close>\<close>_/(3'(| _ |')))\<close> [900, 0] 900)
 
 end