
diff -r 27246f8b2dac -r 890e983cb07b src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Mon Nov 11 18:37:56 2013 +0100
+++ b/src/Doc/IsarImplementation/ML.thy	Mon Nov 11 20:00:53 2013 +0100
@@ -1033,7 +1033,7 @@
   without any message output.
 
   \begin{warn}
-  The actual error channel is accessed via @{ML Output.error_msg}, but
+  The actual error channel is accessed via @{ML Output.error_message}, but
   the old interaction protocol of Proof~General \emph{crashes} if that
   function is used in regular ML code: error output and toplevel
   command failure always need to coincide in classic TTY interaction.




