--- a/src/HOL/Matrix/Compute_Oracle/report.ML	Sun Mar 20 21:20:07 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/report.ML	Sun Mar 20 21:28:11 2011 +0100
@@ -11,9 +11,9 @@
 
 fun timeit f =
     let
-        val t1 = start_timing ()
+        val t1 = Timing.start ()
         val x = f ()
-        val t2 = #message (end_timing t1)
+        val t2 = Timing.message (Timing.result t1)
         val _ = writeln ((report_space ()) ^ "--> "^t2)
     in
         x