--- 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>"