diff -r ff2a637a449e -r fc5066122e68 src/HOL/ex/Code_Lazy_Demo.thy
--- a/src/HOL/ex/Code_Lazy_Demo.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -41,6 +41,8 @@
 
 syntax
   "_llist" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>\<lbrakk>_\<^bold>\<rbrakk>)\<close>)
+syntax_consts
+  "_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>"