src/HOL/Mutabelle/mutabelle_extra.ML

       (* andalso is_executable_thm thy th *))
     (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
 
 fun count x = (length oo filter o equal) x
 
-fun cpu_time description f =
-  let
-    val start = start_timing ()
+fun cpu_time description f =  (* FIXME !? *)
+  let
+    val start = Timing.start ()
     val result = Exn.capture f ()
-    val time = Time.toMilliseconds (#cpu (end_timing start))
+    val time = Time.toMilliseconds (#cpu (Timing.result start))
   in (Exn.release result, (description, time)) end
 (*
 fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   let
     val _ = Output.urgent_message ("Invoking " ^ mtd_name)