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