use_output: Symbol.escape;
authorwenzelm
Sun Jun 20 09:27:24 2004 +0200 (2004-06-20)
changeset 1497665f572245276
parent 14975 2736b0984253
child 14977 77d88064991a
use_output: Symbol.escape;
src/Pure/context.ML
     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);