src/Pure/context.ML
changeset 14976 65f572245276
parent 11819 9283b3c11234
child 14981 e73f8140af78
     1.1 --- a/src/Pure/context.ML	Sun Jun 20 09:27:17 2004 +0200
     1.2 +++ b/src/Pure/context.ML	Sun Jun 20 09:27:24 2004 +0200
     1.3 @@ -72,7 +72,8 @@
     1.4  (* use ML text *)
     1.5  
     1.6  val ml_output = (writeln, error_msg: string -> unit);
     1.7 -fun use_output verb txt = use_text ml_output verb (Symbol.plain_output txt);
     1.8 +
     1.9 +fun use_output verb txt = use_text ml_output verb (Symbol.escape txt);
    1.10  
    1.11  fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) ();
    1.12  fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt);