src/HOL/Matrix/Compute_Oracle/report.ML
changeset 42012 2c3fe3cbebae
parent 37872 d83659570337
     1.1 --- a/src/HOL/Matrix/Compute_Oracle/report.ML	Sun Mar 20 21:20:07 2011 +0100
     1.2 +++ b/src/HOL/Matrix/Compute_Oracle/report.ML	Sun Mar 20 21:28:11 2011 +0100
     1.3 @@ -11,9 +11,9 @@
     1.4  
     1.5  fun timeit f =
     1.6      let
     1.7 -        val t1 = start_timing ()
     1.8 +        val t1 = Timing.start ()
     1.9          val x = f ()
    1.10 -        val t2 = #message (end_timing t1)
    1.11 +        val t2 = Timing.message (Timing.result t1)
    1.12          val _ = writeln ((report_space ()) ^ "--> "^t2)
    1.13      in
    1.14          x