src/Pure/General/output.ML

--- a/src/Pure/General/output.ML	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 11 16:48:02 2011 +0200
@@ -96,7 +96,9 @@
   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 => ());
+  val raw_message_fn =
+    Unsynchronized.ref
+      (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
 end;
 
 fun writeln s = ! Private_Hooks.writeln_fn (output s);