src/Pure/context.ML
changeset 20926 b2f67b947200
parent 20821 bae9a1002d84
child 21518 571b8cd087f8
     1.1 --- a/src/Pure/context.ML	Mon Oct 09 19:37:04 2006 +0200
     1.2 +++ b/src/Pure/context.ML	Mon Oct 09 19:37:05 2006 +0200
     1.3 @@ -58,7 +58,6 @@
     1.4    val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
     1.5    val save: ('a -> 'b) -> 'a -> 'b
     1.6    val >> : (theory -> theory) -> unit
     1.7 -  val ml_output: (string -> unit) * (string -> unit)
     1.8    val use_mltext: string -> bool -> theory option -> unit
     1.9    val use_mltext_theory: string -> bool -> theory -> theory
    1.10    val use_let: string -> string -> string -> theory -> theory
    1.11 @@ -482,10 +481,8 @@
    1.12  
    1.13  (* use ML text *)
    1.14  
    1.15 -val ml_output = (writeln, Output.error_msg);
    1.16 -
    1.17  fun use_output verbose txt =
    1.18 -  Output.ML_errors (use_text ml_output verbose) (Symbol.escape txt);
    1.19 +  Output.ML_errors (use_text Output.ml_output verbose) (Symbol.escape txt);
    1.20  
    1.21  fun use_mltext txt verbose opt_thy = setmp opt_thy (fn () => use_output verbose txt) ();
    1.22  fun use_mltext_theory txt verbose thy = #2 (pass_theory thy (use_output verbose) txt);