diff -r 14841c6e4d5f -r eccc4a13216d src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Sat May 22 13:35:25 2021 +0200
@@ -720,7 +720,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type indexname: "string * int"} \\
+  @{index_ML_type indexname = "string * int"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>indexname\<close> represents indexed names. This is an