--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Tue Oct 01 20:39:16 2024 +0200
@@ -25,8 +25,6 @@
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
- lazy_llist
translations
"\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
"\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"