# HG changeset patch
# User wenzelm
# Date 1087716444 -7200
# Node ID 65f5722452767a3d272da14c4938378e9059e2e6
# Parent  2736b098425335ec9bbaa65dd3fb1c41873f93e0
use_output: Symbol.escape;

diff -r 2736b0984253 -r 65f572245276 src/Pure/context.ML
--- 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);