use_output: Symbol.escape;

--- 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);