--- a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML Fri May 18 15:08:08 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_try0.ML Fri May 18 16:43:38 2012 +0200
@@ -10,8 +10,10 @@
fun init _ = I
fun done _ _ = ()
-fun run id ({pre, (* timeout, *) log, ...}: Mirabelle.run_args) =
- if Try0.try0 (* (SOME timeout) *) NONE ([], [], [], []) pre
+fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time)
+
+fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
+ if TimeLimit.timeLimit (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
then log (try0_tag id ^ "succeeded")
else ()
handle TimeLimit.TimeOut => log (try0_tag id ^ "timeout")