diff -r deab5d9c1ef1 -r 148b78fb70d8 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Fri Sep 10 15:39:55 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Fri Sep 10 15:42:14 2010 +0200
@@ -580,7 +580,7 @@
   \item @{ML_type thm} represents proven propositions.  This is an
   abstract datatype that guarantees that its values have been
   constructed by basic principles of the @{ML_struct Thm} module.
-  Every @{ML thm} value contains a sliding back-reference to the
+  Every @{ML_type thm} value contains a sliding back-reference to the
   enclosing theory, cf.\ \secref{sec:context-theory}.
 
   \item @{ML proofs} specifies the detail of proof recording within