--- a/src/Doc/Implementation/ML.thy Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Doc/Implementation/ML.thy Fri Oct 31 11:18:17 2014 +0100
@@ -1056,9 +1056,7 @@
\begin{warn}
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.
+ this is normally not used directly in user code.
\end{warn}
\end{description}