diff -r 8042869c2072 -r 843dba3d307a src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -454,7 +454,7 @@
 \<close>
 (*<*)
 no_syntax
-  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+  "_list" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 (*>*)
     syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)