--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Thu Oct 01 20:13:32 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Thu Oct 01 20:20:45 2009 +0200
@@ -546,7 +546,7 @@
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML type}{thm}\verb|type thm| \\
- \indexdef{}{ML}{proofs}\verb|proofs: int ref| \\
+ \indexdef{}{ML}{proofs}\verb|proofs: int Unsynchronized.ref| \\
\indexdef{}{ML}{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
\indexdef{}{ML}{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
\indexdef{}{ML}{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\