diff -r 66893c47500d -r 701912f5645a src/ZF/List.thy
--- a/src/ZF/List.thy	Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/List.thy	Fri Aug 23 23:14:39 2024 +0200
@@ -17,12 +17,11 @@
 syntax
  "_Nil" :: i  (\<open>[]\<close>)
  "_List" :: "is \<Rightarrow> i"  (\<open>[(_)]\<close>)
-
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
   "[x]"         == "CONST Cons(x, [])"
   "[]"          == "CONST Nil"
-
+syntax_consts "_List" \<rightleftharpoons> Cons
 
 consts
   length :: "i\<Rightarrow>i"