# HG changeset patch
# User wenzelm
# Date 1728472015 -7200
# Node ID 2b949a3bfaac124243524bd9af58273e89098da0
# Parent  d90869a85f60baa46dc935926a844fd89097ae04
more syntax bundles;

diff -r d90869a85f60 -r 2b949a3bfaac src/Doc/Codegen/Setup.thy
--- a/src/Doc/Codegen/Setup.thy	Tue Oct 08 23:31:06 2024 +0200
+++ b/src/Doc/Codegen/Setup.thy	Wed Oct 09 13:06:55 2024 +0200
@@ -10,13 +10,7 @@
 ML_file \<open>../antiquote_setup.ML\<close>
 ML_file \<open>../more_antiquote.ML\<close>
 
-no_syntax (output)
-  "_constrain" :: "logic => type => logic"  (\<open>_::_\<close> [4, 0] 3)
-  "_constrain" :: "prop' => type => prop'"  (\<open>_::_\<close> [4, 0] 3)
-
-syntax (output)
-  "_constrain" :: "logic => type => logic"  (\<open>_ :: _\<close> [4, 0] 3)
-  "_constrain" :: "prop' => type => prop'"  (\<open>_ :: _\<close> [4, 0] 3)
+unbundle constrain_space_syntax
 
 declare [[default_code_width = 74]]
 
diff -r d90869a85f60 -r 2b949a3bfaac src/Doc/Tutorial/ToyList/ToyList.thy
--- a/src/Doc/Tutorial/ToyList/ToyList.thy	Tue Oct 08 23:31:06 2024 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy	Wed Oct 09 13:06:55 2024 +0200
@@ -9,7 +9,8 @@
 the concrete syntax and name space of theory \<^theory>\<open>Main\<close> as follows.
 \<close>
 
-no_notation Nil  ("[]") and Cons  (infixr "#" 65) and append  (infixr "@" 65)
+unbundle no list_syntax
+no_notation append  (infixr "@" 65)
 hide_type list
 hide_const rev
 
diff -r d90869a85f60 -r 2b949a3bfaac src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy	Tue Oct 08 23:31:06 2024 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy	Wed Oct 09 13:06:55 2024 +0200
@@ -7,14 +7,7 @@
 imports Imperative_HOL "HOL-Library.LaTeXsugar"
 begin
 
-(* type constraints with spacing *)
-no_syntax (output)
-  "_constrain" :: "logic => type => logic"  (\<open>_::_\<close> [4, 0] 3)
-  "_constrain" :: "prop' => type => prop'"  (\<open>_::_\<close> [4, 0] 3)
-
-syntax (output)
-  "_constrain" :: "logic => type => logic"  (\<open>_ :: _\<close> [4, 0] 3)
-  "_constrain" :: "prop' => type => prop'"  (\<open>_ :: _\<close> [4, 0] 3)
+unbundle constrain_space_syntax
 (*>*)
 
 text \<open>
diff -r d90869a85f60 -r 2b949a3bfaac src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Tue Oct 08 23:31:06 2024 +0200
+++ b/src/HOL/Library/OptionalSugar.thy	Wed Oct 09 13:06:55 2024 +0200
@@ -51,14 +51,7 @@
   "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
   "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
 
-(* type constraints with spacing *)
-no_syntax (output)
-  "_constrain" :: "logic => type => logic"  (\<open>_::_\<close> [4, 0] 3)
-  "_constrain" :: "prop' => type => prop'"  (\<open>_::_\<close> [4, 0] 3)
-
-syntax (output)
-  "_constrain" :: "logic => type => logic"  (\<open>_ :: _\<close> [4, 0] 3)
-  "_constrain" :: "prop' => type => prop'"  (\<open>_ :: _\<close> [4, 0] 3)
+unbundle constrain_space_syntax
 
 
 (* sorts as intersections *)
diff -r d90869a85f60 -r 2b949a3bfaac src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Oct 08 23:31:06 2024 +0200
+++ b/src/Pure/Pure.thy	Wed Oct 09 13:06:55 2024 +0200
@@ -1575,6 +1575,20 @@
   qed
 qed
 
+
+section \<open>Misc\<close>
+
+bundle constrain_space_syntax  \<comment> \<open>type constraints with spacing\<close>
+begin
+no_syntax (output)
+  "_constrain" :: "logic => type => logic"  (\<open>_::_\<close> [4, 0] 3)
+  "_constrain" :: "prop' => type => prop'"  (\<open>_::_\<close> [4, 0] 3)
+syntax (output)
+  "_constrain" :: "logic => type => logic"  (\<open>_ :: _\<close> [4, 0] 3)
+  "_constrain" :: "prop' => type => prop'"  (\<open>_ :: _\<close> [4, 0] 3)
+end
+
+
 declare [[ML_write_global = false]]
 
 ML_command \<open>\<^assert> (not (can ML_command \<open>() handle _ => ()\<close>))\<close>