--- 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>