diff -r 5ea48342e0ae -r 6d34c2bedaa3 src/ZF/List.thy
--- a/src/ZF/List.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/ZF/List.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -19,9 +19,9 @@
 syntax
   "" :: "i \<Rightarrow> list_args"  (\<open>_\<close>)
   "_List_args" :: "[i, list_args] \<Rightarrow> list_args"  (\<open>_,/ _\<close>)
-  "_List" :: "list_args \<Rightarrow> i"  (\<open>[(_)]\<close>)
+  "_List" :: "list_args \<Rightarrow> i"  (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
 syntax_consts
-  "_List_args" "_List" \<rightleftharpoons> Cons
+  Cons
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
   "[x]"         == "CONST Cons(x, [])"