--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sun Mar 20 21:44:38 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sun Mar 20 22:08:12 2011 +0100
@@ -211,12 +211,9 @@
val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
-fun cpu_time description f = (* FIXME !? *)
- let
- val start = Timing.start ()
- val result = Exn.capture f ()
- val time = Time.toMilliseconds (#cpu (Timing.result start))
- in (Exn.release result, (description, time)) end
+fun cpu_time description e =
+ let val ({cpu, ...}, result) = Timing.timing e ()
+ in (result, (description, Time.toMilliseconds cpu)) end
fun compile_term compilation options ctxt t =
let