# HG changeset patch
# User wenzelm
# Date 1724878485 -7200
# Node ID 70076ba563d207e0184a23e7782214058b8624ea
# Parent  713424d012fdbc04453c189d02719b80287a5b25
more specific "args" syntax, to support more markup for syntax consts;

diff -r 713424d012fd -r 70076ba563d2 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -453,7 +453,7 @@
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
 
-    syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
+    syntax "_list" :: "list_args \<Rightarrow> 'a list" ("[(_)]")
 
 text \<open>\blankline\<close>
 
diff -r 713424d012fd -r 70076ba563d2 src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -79,13 +79,16 @@
 
 (*<*)
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
+nonterminal mtuple_args
 syntax
-  "_MTuple"      :: "['a, args] \<Rightarrow> 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+  "" :: "'a \<Rightarrow> mtuple_args"  ("_")
+  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  ("_,/ _")
+  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 syntax_consts
-  "_MTuple"     == MPair
+  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
 translations
-  "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
-  "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
 
 
 definition keysFor :: "msg set \<Rightarrow> key set" where
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Auth/Message.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -49,10 +49,13 @@
 
 
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
+nonterminal mtuple_args
 syntax
-  "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
+  "" :: "'a \<Rightarrow> mtuple_args"  ("_")
+  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  ("_,/ _")
+  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 syntax_consts
-  "_MTuple" \<rightleftharpoons> MPair
+  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
 translations
   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Codegenerator_Test/Code_Lazy_Test.thy
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -23,8 +23,13 @@
 code_lazy_type llist
 
 no_notation lazy_llist ("_")
-syntax "_llist" :: "args => 'a list"    ("\<^bold>[(_)\<^bold>]")
-syntax_consts "_llist" == lazy_llist
+nonterminal llist_args
+syntax
+  "" :: "'a \<Rightarrow> llist_args"  ("_")
+  "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  ("_,/ _")
+  "_llist" :: "llist_args => 'a list"    ("\<^bold>[(_)\<^bold>]")
+syntax_consts
+  "_llist_args" "_llist" == lazy_llist
 translations
   "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
   "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -348,7 +348,13 @@
 
 subsection \<open>List-style syntax for polynomials\<close>
 
-syntax "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
+nonterminal poly_args
+syntax
+  "" :: "'a \<Rightarrow> poly_args"  ("_")
+  "_poly_args" :: "'a \<Rightarrow> poly_args \<Rightarrow> poly_args"  ("_,/ _")
+  "_poly" :: "poly_args \<Rightarrow> 'a poly"  ("[:(_):]")
+syntax_consts
+  "_poly_args" "_poly" \<rightleftharpoons> pCons
 translations
   "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
   "[:x:]" \<rightleftharpoons> "CONST pCons x 0"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -178,12 +178,13 @@
     (infixl "\<union>\<natural>" 65) where
   "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
 
+nonterminal convex_pd_args
 syntax
-  "_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>")
-
+  "" :: "logic \<Rightarrow> convex_pd_args"  ("_")
+  "_convex_pd_args" :: "logic \<Rightarrow> convex_pd_args \<Rightarrow> convex_pd_args"  ("_,/ _")
+  "_convex_pd" :: "convex_pd_args \<Rightarrow> logic"  ("{_}\<natural>")
 syntax_consts
-  "_convex_pd" == convex_add
-
+  "_convex_pd_args" "_convex_pd" == convex_add
 translations
   "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
   "{x}\<natural>" == "CONST convex_unit\<cdot>x"
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
diff -r 713424d012fd -r 70076ba563d2 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -133,12 +133,13 @@
     (infixl "\<union>\<flat>" 65) where
   "xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
 
+nonterminal lower_pd_args
 syntax
-  "_lower_pd" :: "args \<Rightarrow> logic" ("{_}\<flat>")
-
+  "" :: "logic \<Rightarrow> lower_pd_args"  ("_")
+  "_lower_pd_args" :: "logic \<Rightarrow> lower_pd_args \<Rightarrow> lower_pd_args"  ("_,/ _")
+  "_lower_pd" :: "lower_pd_args \<Rightarrow> logic" ("{_}\<flat>")
 syntax_consts
-  "_lower_pd" == lower_add
-
+  "_lower_pd_args" "_lower_pd" == lower_add
 translations
   "{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
   "{x}\<flat>" == "CONST lower_unit\<cdot>x"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -40,8 +40,13 @@
 definition ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c"
   where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
 
-syntax "_stuple" :: "[logic, args] \<Rightarrow> logic"  ("(1'(:_,/ _:'))")
-syntax_consts "_stuple" \<rightleftharpoons> spair
+nonterminal stuple_args
+syntax
+  "" :: "logic \<Rightarrow> stuple_args"  ("_")
+  "_stuple_args" :: "logic \<Rightarrow> stuple_args \<Rightarrow> stuple_args"  ("_,/ _")
+  "_stuple" :: "[logic, stuple_args] \<Rightarrow> logic"  ("(1'(:_,/ _:'))")
+syntax_consts
+  "_stuple_args" "_stuple" \<rightleftharpoons> spair
 translations
   "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
   "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -131,12 +131,13 @@
     (infixl "\<union>\<sharp>" 65) where
   "xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
 
+nonterminal upper_pd_args
 syntax
-  "_upper_pd" :: "args \<Rightarrow> logic" ("{_}\<sharp>")
-
+  "" :: "logic \<Rightarrow> upper_pd_args"  ("_")
+  "_upper_pd_args" :: "logic \<Rightarrow> upper_pd_args \<Rightarrow> upper_pd_args"  ("_,/ _")
+  "_upper_pd" :: "upper_pd_args \<Rightarrow> logic"  ("{_}\<sharp>")
 syntax_consts
-  "_upper_pd" == upper_add
-
+  "_upper_pd_args" "_upper_pd" == upper_add
 translations
   "{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
   "{x}\<sharp>" == "CONST upper_unit\<cdot>x"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -164,12 +164,13 @@
 lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer
   by simp
 
+nonterminal fset_args
 syntax
-  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
-
+  "" :: "'a \<Rightarrow> fset_args"  ("_")
+  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  ("_,/ _")
+  "_fset" :: "fset_args => 'a fset"  ("{|(_)|}")
 syntax_consts
-  "_insert_fset" == finsert
-
+  "_fset_args" "_fset" == finsert
 translations
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -91,10 +91,13 @@
   "\<lambda>a M b. if b = a then Suc (M b) else M b"
 by (rule add_mset_in_multiset)
 
+nonterminal multiset_args
 syntax
-  "_multiset" :: "args \<Rightarrow> 'a multiset"    ("{#(_)#}")
+  "" :: "'a \<Rightarrow> multiset_args"  ("_")
+  "_multiset_args" :: "'a \<Rightarrow> multiset_args \<Rightarrow> multiset_args"  ("_,/ _")
+  "_multiset" :: "multiset_args \<Rightarrow> 'a multiset"    ("{#(_)#}")
 syntax_consts
-  "_multiset" == add_mset
+  "_multiset_args" "_multiset" == add_mset
 translations
   "{#x, xs#}" == "CONST add_mset x {#xs#}"
   "{#x#}" == "CONST add_mset x {#}"
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#[]"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -48,13 +48,16 @@
 
 
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
+nonterminal mtuple_args
 syntax
-  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+  "" :: "'a \<Rightarrow> mtuple_args"  ("_")
+  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  ("_,/ _")
+  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 syntax_consts
-  "_MTuple"     == MPair
+  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
 translations
-  "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
-  "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
 
 
 definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Prolog/Test.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -16,13 +16,18 @@
   Nil   :: "'a list"                                  ("[]")
   Cons  :: "'a => 'a list => 'a list"                 (infixr "#"  65)
 
-syntax
-  (* list Enumeration *)
-  "_list"     :: "args => 'a list"                          ("[(_)]")
+text \<open>List enumeration\<close>
 
+nonterminal list_args
+syntax
+  "" :: "'a \<Rightarrow> list_args"  ("_")
+  "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args"  ("_,/ _")
+  "_list" :: "list_args => 'a list"    ("[(_)]")
+syntax_consts
+  "_list_args" "_list" == Cons
 translations
-  "[x, xs]"     == "x#[xs]"
-  "[x]"         == "x#[]"
+  "[x, xs]" == "x#[xs]"
+  "[x]" == "x#[]"
 
 typedecl person
 
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -95,12 +95,13 @@
 
 end
 
+nonterminal fset_args
 syntax
-  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
-
+  "" :: "'a \<Rightarrow> fset_args"  ("_")
+  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  ("_,/ _")
+  "_fset" :: "fset_args => 'a fset"  ("{|(_)|}")
 syntax_consts
-  "_insert_fset" == fcons
-
+  "_fset_args" "_fset" == fcons
 translations
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Quotient_Examples/Quotient_FSet.thy
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -288,12 +288,13 @@
   "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   is "Cons" by auto
 
+nonterminal fset_args
 syntax
-  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
-
+  "" :: "'a \<Rightarrow> fset_args"  ("_")
+  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  ("_,/ _")
+  "_fset" :: "fset_args => 'a fset"  ("{|(_)|}")
 syntax_consts
-  "_insert_fset" == insert_fset
-
+  "_fset_args" "_fset" == insert_fset
 translations
   "{|x, xs|}" == "CONST insert_fset x {|xs|}"
   "{|x|}"     == "CONST insert_fset x {||}"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -68,10 +68,13 @@
 
 
 (*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
+nonterminal mtuple_args
 syntax
-  "_MTuple"      :: "['a, args] \<Rightarrow> 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+  "" :: "'a \<Rightarrow> mtuple_args"  ("_")
+  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  ("_,/ _")
+  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 syntax_consts
-  "_MTuple"     == MPair
+  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
 translations
   "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Set.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -143,10 +143,13 @@
 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
 
+nonterminal finset_args
 syntax
-  "_Finset" :: "args \<Rightarrow> 'a set"    ("{(_)}")
+  "" :: "'a \<Rightarrow> finset_args"  ("_")
+  "_Finset_args" :: "'a \<Rightarrow> finset_args \<Rightarrow> finset_args"  ("_,/ _")
+  "_Finset" :: "finset_args \<Rightarrow> 'a set"    ("{(_)}")
 syntax_consts
-  "_Finset" \<rightleftharpoons> insert
+  "_Finset_args" "_Finset" \<rightleftharpoons> insert
 translations
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"
diff -r 713424d012fd -r 70076ba563d2 src/HOL/ex/Code_Lazy_Demo.thy
--- a/src/HOL/ex/Code_Lazy_Demo.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -39,8 +39,13 @@
   = LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>") 
   | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
 
-syntax "_llist" :: "args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
-syntax_consts "_llist" == LCons
+nonterminal llist_args
+syntax
+  "" :: "'a \<Rightarrow> llist_args"  ("_")
+  "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  ("_,/ _")
+  "_llist" :: "llist_args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
+syntax_consts
+  "_llist_args" "_llist" == LCons
 translations
   "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
   "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"