# HG changeset patch
# User wenzelm
# Date 1310417429 -7200
# Node ID ef8375a4dae4850e4725d551536490e7a4ae60bf
# Parent  d93a69672362a0a418c75870acbfec3761bc9761
made SML/NJ happy;
tuned error;

diff -r d93a69672362 -r ef8375a4dae4 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Jul 11 22:19:11 2011 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 11 22:50:29 2011 +0200
@@ -96,9 +96,8 @@
   val prompt_fn = Unsynchronized.ref raw_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
-  val raw_message_fn =
-    Unsynchronized.ref
-      (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
+  val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
+    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode");
 end;
 
 fun writeln s = ! Private_Hooks.writeln_fn (output s);