diff -r c48d536231fe -r 96a4765ba7d1 src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Doc/Implementation/Integration.thy	Thu Apr 16 14:18:32 2015 +0200
@@ -62,7 +62,7 @@
   for an empty toplevel state.
 
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
-  state if available, otherwise it raises @{ML Toplevel.UNDEF}.
+  state if available, otherwise it raises an error.
 
   \end{description}
 \<close>