--- 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.