
diff -r ff2a637a449e -r fc5066122e68 src/HOL/Codegenerator_Test/Code_Lazy_Test.thy
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -25,6 +25,8 @@
 no_notation lazy_llist (\<open>_\<close>)
 syntax
   "_llist" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>[_\<^bold>])\<close>)
+syntax_consts
+  "_llist" \<rightleftharpoons> lazy_llist
 translations
   "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
   "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"




