made SML/NJ happy;
authorwenzelm
Mon Jul 11 22:50:29 2011 +0200 (2011-07-11)
changeset 43760ef8375a4dae4
parent 43759 d93a69672362
child 43761 e72ba84ae58f
made SML/NJ happy;
tuned error;
src/Pure/General/output.ML
     1.1 --- a/src/Pure/General/output.ML	Mon Jul 11 22:19:11 2011 +0200
     1.2 +++ b/src/Pure/General/output.ML	Mon Jul 11 22:50:29 2011 +0200
     1.3 @@ -96,9 +96,8 @@
     1.4    val prompt_fn = Unsynchronized.ref raw_stdout;
     1.5    val status_fn = Unsynchronized.ref (fn _: output => ());
     1.6    val report_fn = Unsynchronized.ref (fn _: output => ());
     1.7 -  val raw_message_fn =
     1.8 -    Unsynchronized.ref
     1.9 -      (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
    1.10 +  val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
    1.11 +    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode");
    1.12  end;
    1.13  
    1.14  fun writeln s = ! Private_Hooks.writeln_fn (output s);