--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Dec 03 09:55:45 2010 +0100
@@ -114,13 +114,14 @@
(** quickcheck **)
fun invoke_quickcheck change_options quickcheck_generator thy t =
- TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
+ TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
(fn _ =>
case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
false [] [t] of
(NONE, _) => (NoCex, ([], NONE))
| (SOME _, _) => (GenuineCex, ([], NONE))) ()
- handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
+ handle TimeLimit.TimeOut =>
+ (Timeout, ([("timelimit", Real.floor !Auto_Tools.time_limit)], NONE))
fun quickcheck_mtd change_options quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)