# HG changeset patch
# User wenzelm
# Date 1728401191 -7200
# Node ID 072cc2a92ba3bb3b881b195d7f8efb7da3bb2d00
# Parent  dff7dfd8dce371b720d4f515b089a22920eabf0a
clarified bundles for list syntax;

diff -r dff7dfd8dce3 -r 072cc2a92ba3 NEWS
--- a/NEWS	Tue Oct 08 16:15:31 2024 +0200
+++ b/NEWS	Tue Oct 08 17:26:31 2024 +0200
@@ -65,7 +65,8 @@
 notably like this:
 
   unbundle no list_syntax
-  unbundle no listcompr_syntax
+  unbundle no list_enumeration_syntax
+  unbundle no list_comprehension_syntax
   unbundle no rtrancl_syntax
   unbundle no trancl_syntax
   unbundle no reflcl_syntax
diff -r dff7dfd8dce3 -r 072cc2a92ba3 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Oct 08 16:15:31 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Oct 08 17:26:31 2024 +0200
@@ -360,8 +360,7 @@
       "[x, xs]" == "x # [xs]"
       "[x]" == "x # []"
 
-    no_notation Nil  (\<open>[]\<close>) and Cons  (infixr \<open>#\<close> 65)
-
+    unbundle no list_syntax
     hide_type list
     hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list list_all
 
@@ -451,7 +450,7 @@
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
 (*<*)
-unbundle no list_syntax
+unbundle no list_enumeration_syntax
 (*>*)
     syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
 
diff -r dff7dfd8dce3 -r 072cc2a92ba3 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Tue Oct 08 16:15:31 2024 +0200
+++ b/src/HOL/Induct/SList.thy	Tue Oct 08 17:26:31 2024 +0200
@@ -83,7 +83,7 @@
 no_translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
-no_notation Nil  (\<open>[]\<close>) and Cons  (infixr \<open>#\<close> 65)
+unbundle no list_syntax
 
 definition
   Nil       :: "'a list"                               (\<open>[]\<close>) where
diff -r dff7dfd8dce3 -r 072cc2a92ba3 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Oct 08 16:15:31 2024 +0200
+++ b/src/HOL/List.thy	Tue Oct 08 17:26:31 2024 +0200
@@ -18,6 +18,12 @@
 where
   "tl [] = []"
 
+bundle list_syntax
+begin
+notation Nil  (\<open>[]\<close>)
+  and Cons  (infixr \<open>#\<close> 65)
+end
+
 datatype_compat list
 
 lemma [case_names Nil Cons, cases type: list]:
@@ -45,17 +51,14 @@
 
 text \<open>List enumeration\<close>
 
-syntax
-  "_list" :: "args \<Rightarrow> 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
-translations
-  "[x, xs]" \<rightleftharpoons> "x#[xs]"
-  "[x]" \<rightleftharpoons> "x#[]"
-
-bundle list_syntax
+open_bundle list_enumeration_syntax
 begin
 syntax
   "_list" :: "args \<Rightarrow> 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 end
+translations
+  "[x, xs]" \<rightleftharpoons> "x#[xs]"
+  "[x]" \<rightleftharpoons> "x#[]"
 
 
 subsection \<open>Basic list processing functions\<close>
@@ -447,6 +450,8 @@
 
 nonterminal lc_qual and lc_quals
 
+open_bundle list_comprehension_syntax
+begin
 syntax
   "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  (\<open>[_ . __\<close>)
   "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  (\<open>_ \<leftarrow> _\<close>)
@@ -457,12 +462,6 @@
 
 syntax (ASCII)
   "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  (\<open>_ <- _\<close>)
-
-bundle listcompr_syntax
-begin
-syntax
-  "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  (\<open>[_ . __\<close>)
-  "_lc_end" :: "lc_quals" (\<open>]\<close>)
 end
 
 parse_translation \<open>