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