diff -r 713424d012fd -r 70076ba563d2 src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -69,9 +69,12 @@
 
 subsection \<open>List enumeration\<close>
 
+nonterminal llist_args
 syntax
-  "_totlist" :: "args \<Rightarrow> 'a Seq"  ("[(_)!]")
-  "_partlist" :: "args \<Rightarrow> 'a Seq"  ("[(_)?]")
+  "" :: "'a \<Rightarrow> llist_args"  ("_")
+  "_list_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  ("_,/ _")
+  "_totlist" :: "llist_args \<Rightarrow> 'a Seq"  ("[(_)!]")
+  "_partlist" :: "llist_args \<Rightarrow> 'a Seq"  ("[(_)?]")
 syntax_consts
   "_totlist" "_partlist" \<rightleftharpoons> Consq
 translations