src/HOL/Codegenerator_Test/Code_Lazy_Test.thy
changeset 80768 c7723cc15de8
parent 69597 ff784d5a5bfb
child 80786 70076ba563d2
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -24,6 +24,7 @@
 
 no_notation lazy_llist ("_")
 syntax "_llist" :: "args => 'a list"    ("\<^bold>[(_)\<^bold>]")
+syntax_consts "_llist" == lazy_llist
 translations
   "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
   "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"