# HG changeset patch
# User wenzelm
# Date 1728473119 -7200
# Node ID 52ed95fa465665929d0aefbd51dc5ca9f589a890
# Parent  2b949a3bfaac124243524bd9af58273e89098da0
more syntax bundles, less clones;

diff -r 2b949a3bfaac -r 52ed95fa4656 src/HOL/Library/Datatype_Records.thy
--- a/src/HOL/Library/Datatype_Records.thy	Wed Oct 09 13:06:55 2024 +0200
+++ b/src/HOL/Library/Datatype_Records.thy	Wed Oct 09 13:25:19 2024 +0200
@@ -26,41 +26,10 @@
   \<^item> extensible records are not supported
 \<close>
 
-no_syntax
-  "_constify"           :: "id => ident"                        (\<open>_\<close>)
-  "_constify"           :: "longid => ident"                    (\<open>_\<close>)
-
-  "_field_type"         :: "ident => type => field_type"        (\<open>(\<open>indent=2 notation=\<open>infix field type\<close>\<close>_ ::/ _)\<close>)
-  ""                    :: "field_type => field_types"          (\<open>_\<close>)
-  "_field_types"        :: "field_type => field_types => field_types"    (\<open>_,/ _\<close>)
-  "_record_type"        :: "field_types => type"                (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_\<rparr>)\<close>)
-  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_,/ (\<open>indent=2 notation=\<open>infix more type\<close>\<close>\<dots> ::/ _)\<rparr>)\<close>)
-
-  "_field"              :: "ident => 'a => field"               (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>_ =/ _)\<close>)
-  ""                    :: "field => fields"                    (\<open>_\<close>)
-  "_fields"             :: "field => fields => fields"          (\<open>_,/ _\<close>)
-  "_record"             :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_\<rparr>)\<close>)
-  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_,/ (\<open>indent=2 notation=\<open>infix more value\<close>\<close>\<dots> =/ _)\<rparr>)\<close>)
+open_bundle datatype_record_syntax
+begin
 
-  "_field_update"       :: "ident => 'a => field_update"        (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>_ :=/ _)\<close>)
-  ""                    :: "field_update => field_updates"      (\<open>_\<close>)
-  "_field_updates"      :: "field_update => field_updates => field_updates"  (\<open>_,/ _\<close>)
-  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>\<lparr>_\<rparr>)\<close> [900, 0] 900)
-
-no_syntax (ASCII)
-  "_record_type"        :: "field_types => type"                (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _ |'))\<close>)
-  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _,/ (\<open>indent=2 notation=\<open>infix more type\<close>\<close>... ::/ _) |'))\<close>)
-  "_record"             :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _ |'))\<close>)
-  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _,/ (\<open>indent=2 notation=\<open>infix more value\<close>\<close>... =/ _) |'))\<close>)
-  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>'(| _ |'))\<close> [900, 0] 900)
-
-(* copied and adapted from Record.thy *)
-
-nonterminal
-  field and
-  fields and
-  field_update and
-  field_updates
+unbundle no record_syntax
 
 syntax
   "_constify"               :: "id => ident"                        (\<open>_\<close>)
@@ -80,6 +49,8 @@
   "_datatype_record_scheme" :: "fields => 'a => 'a"                 (\<open>(3'(| _,/ (2... =/ _) |'))\<close>)
   "_datatype_record_update" :: "'a => field_updates => 'b"          (\<open>_/(3'(| _ |'))\<close> [900, 0] 900)
 
+end
+
 named_theorems datatype_record_update
 
 ML_file \<open>datatype_records.ML\<close>
diff -r 2b949a3bfaac -r 52ed95fa4656 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Wed Oct 09 13:06:55 2024 +0200
+++ b/src/HOL/Record.thy	Wed Oct 09 13:25:19 2024 +0200
@@ -422,6 +422,9 @@
   field_update and
   field_updates
 
+open_bundle record_syntax
+begin
+
 syntax
   "_constify"           :: "id => ident"                        (\<open>_\<close>)
   "_constify"           :: "longid => ident"                    (\<open>_\<close>)
@@ -450,6 +453,8 @@
   "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _,/ (\<open>indent=2 notation=\<open>infix more value\<close>\<close>... =/ _) |'))\<close>)
   "_record_update"      :: "'a => field_updates => 'b"          (\<open>(\<open>open_block notation=\<open>mixfix record update\<close>\<close>_/(3'(| _ |')))\<close> [900, 0] 900)
 
+end
+
 
 subsection \<open>Record package\<close>