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>