src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML

   Predicate_Compile_Aux.mk_bind New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
   
 
 val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
 
-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 compile_term compilation options ctxt t =
   let
     val thy = Theory.copy (ProofContext.theory_of ctxt)