diff -r 713424d012fd -r 70076ba563d2 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -453,7 +453,7 @@
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
 
-    syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
+    syntax "_list" :: "list_args \<Rightarrow> 'a list" ("[(_)]")
 
 text \<open>\blankline\<close>