diff -r f27f66e9adca -r 66a8113ac23e src/ZF/List.thy
--- a/src/ZF/List.thy	Thu Aug 29 11:39:50 2024 +0200
+++ b/src/ZF/List.thy	Thu Aug 29 11:43:14 2024 +0200
@@ -15,9 +15,13 @@
 
 notation Nil (\<open>[]\<close>)
 
+nonterminal list_args
 syntax
- "_List" :: "is \<Rightarrow> i"  (\<open>[(_)]\<close>)
-syntax_consts "_List" \<rightleftharpoons> Cons
+  "" :: "i \<Rightarrow> list_args"  (\<open>_\<close>)
+  "_List_args" :: "[i, list_args] \<Rightarrow> list_args"  (\<open>_,/ _\<close>)
+  "_List" :: "list_args \<Rightarrow> i"  (\<open>[(_)]\<close>)
+syntax_consts
+  "_List_args" "_List" \<rightleftharpoons> Cons
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
   "[x]"         == "CONST Cons(x, [])"