--- a/src/Pure/context.ML Sun Jun 20 09:27:17 2004 +0200
+++ b/src/Pure/context.ML Sun Jun 20 09:27:24 2004 +0200
@@ -72,7 +72,8 @@
(* use ML text *)
val ml_output = (writeln, error_msg: string -> unit);
-fun use_output verb txt = use_text ml_output verb (Symbol.plain_output txt);
+
+fun use_output verb txt = use_text ml_output verb (Symbol.escape txt);
fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) ();
fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt);