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 (\_\) syntax "_llist" :: "args => 'a list" (\(\indent=1 notation=\mixfix lazy list enumeration\\\<^bold>[_\<^bold>])\) +syntax_consts + "_llist" \ lazy_llist translations "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"