src/Doc/IsarImplementation/ML.thy

   perfectly legal alternative: it means that the error is absorbed
   without any message output.
 
   \begin{warn}
   The actual error channel is accessed via @{ML Output.error_msg}, but
-  the interaction protocol of Proof~General \emph{crashes} if that
+  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.
   \end{warn}
 
   \end{description}