more robust 'no_syntax' via bundles;

--- a/src/Doc/Datatypes/Datatypes.thy	Tue Oct 01 21:30:59 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Oct 01 21:35:31 2024 +0200
@@ -453,8 +453,7 @@
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
 (*<*)
-no_syntax
-  "_list" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
+unbundle no_list_syntax
 (*>*)
     syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
 

--- a/src/HOL/List.thy	Tue Oct 01 21:30:59 2024 +0200
+++ b/src/HOL/List.thy	Tue Oct 01 21:35:31 2024 +0200
@@ -46,10 +46,16 @@
 text \<open>List enumeration\<close>
 
 syntax
-  "_list" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
+  "_list" :: "args \<Rightarrow> 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 translations
-  "[x, xs]" == "x#[xs]"
-  "[x]" == "x#[]"
+  "[x, xs]" \<rightleftharpoons> "x#[xs]"
+  "[x]" \<rightleftharpoons> "x#[]"
+
+bundle no_list_syntax
+begin
+no_syntax
+  "_list" :: "args \<Rightarrow> 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
+end
 
 
 subsection \<open>Basic list processing functions\<close>
@@ -451,6 +457,13 @@
 syntax (ASCII)
   "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  (\<open>_ <- _\<close>)
 
+bundle no_listcompr_syntax
+begin
+no_syntax
+  "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  (\<open>[_ . __\<close>)
+  "_lc_end" :: "lc_quals" (\<open>]\<close>)
+end
+
 parse_translation \<open>
 let
   val NilC = Syntax.const \<^const_syntax>\<open>Nil\<close>;