src/Pure/General/output.ML

--- a/src/Pure/General/output.ML	Sun Mar 01 14:45:23 2009 +0100
+++ b/src/Pure/General/output.ML	Sun Mar 01 16:21:33 2009 +0100
@@ -135,7 +135,7 @@
     let
       val start = start_timing ();
       val result = Exn.capture e ();
-      val end_msg = end_timing start;
+      val end_msg = #message (end_timing start);
       val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
     in Exn.release result end
   else e ();