diff -r 83596aea48cb -r dd59daa3c37a src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -452,8 +452,11 @@
 \noindent
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
-
-    syntax "_list" :: "list_args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
+(*<*)
+no_syntax
+  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+(*>*)
+    syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
 
 text \<open>\blankline\<close>