diff -r 713424d012fd -r 70076ba563d2 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/List.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -42,13 +42,16 @@
 
 lemmas set_simps = list.set (* legacy *)
 
+
+text \<open>List enumeration\<close>
+
+nonterminal list_args
 syntax
-  \<comment> \<open>list Enumeration\<close>
-  "_list" :: "args => 'a list"    ("[(_)]")
-
+  "" :: "'a \<Rightarrow> list_args"  ("_")
+  "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args"  ("_,/ _")
+  "_list" :: "list_args => 'a list"    ("[(_)]")
 syntax_consts
-  "_list" == Cons
-
+  "_list_args" "_list" == Cons
 translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"