diff -r ebe2253e5c0e -r 93e7935d4cb5 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Mon Oct 25 11:01:00 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Mon Oct 25 11:16:23 2010 +0200
@@ -1207,10 +1207,10 @@
 
   \begin{description}
 
-  \item @{text "@{assert}"} inlines a function @{text "bool \<Rightarrow> unit"}
-  that raises @{ML Fail} if the argument is @{ML false}.  Due to
-  inlining the source position of failed assertions is included in the
-  error output.
+  \item @{text "@{assert}"} inlines a function
+  @{ML_type "bool -> unit"} that raises @{ML Fail} if the argument is
+  @{ML false}.  Due to inlining the source position of failed
+  assertions is included in the error output.
 
   \end{description}
 *}