diff -r 83596aea48cb -r dd59daa3c37a src/HOL/ex/Code_Lazy_Demo.thy
--- a/src/HOL/ex/Code_Lazy_Demo.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -39,13 +39,10 @@
   = LNil (\<open>\<^bold>\<lbrakk>\<^bold>\<rbrakk>\<close>) 
   | LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>###\<close> 65)
 
-nonterminal llist_args
 syntax
-  "" :: "'a \<Rightarrow> llist_args"  (\<open>_\<close>)
-  "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  (\<open>_,/ _\<close>)
-  "_llist" :: "llist_args => 'a list"    (\<open>\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>\<close>)
+  "_llist" :: "args => 'a list"    (\<open>\<^bold>\<lbrakk>(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>\<rbrakk>\<close>)
 syntax_consts
-  "_llist_args" "_llist" == LCons
+  LCons
 translations
   "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
   "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"