src/Pure/General/output.ML
changeset 43748 c70bd78ec83c
parent 43746 a41f618c641d
child 43760 ef8375a4dae4
     1.1 --- a/src/Pure/General/output.ML	Mon Jul 11 15:56:30 2011 +0200
     1.2 +++ b/src/Pure/General/output.ML	Mon Jul 11 16:48:02 2011 +0200
     1.3 @@ -96,7 +96,9 @@
     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 = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
     1.8 +  val raw_message_fn =
     1.9 +    Unsynchronized.ref
    1.10 +      (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
    1.11  end;
    1.12  
    1.13  fun writeln s = ! Private_Hooks.writeln_fn (output s);