--- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu Oct 01 20:13:32 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Oct 01 20:20:45 2009 +0200
@@ -277,7 +277,7 @@
\begin{mldecls}
\indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
\indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
- \indexdef{}{ML}{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
+ \indexdef{}{ML}{setmp}\verb|setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
\end{mldecls}
\begin{description}