| changeset 51058 | 98c48d023136 |
| parent 48985 | 5386df44a037 |
| child 51295 | 71fc3776c453 |
--- a/src/Doc/IsarImplementation/ML.thy Sat Jan 26 16:10:50 2013 +0100 +++ b/src/Doc/IsarImplementation/ML.thy Sat Jan 26 16:30:47 2013 +0100 @@ -1050,7 +1050,7 @@ \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}