--- a/src/HOL/IsaMakefile Fri May 18 15:08:08 2012 +0200
+++ b/src/HOL/IsaMakefile Fri May 18 16:43:38 2012 +0200
@@ -1334,6 +1334,7 @@
Mirabelle/Tools/mirabelle_refute.ML \
Mirabelle/Tools/mirabelle_sledgehammer.ML \
Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \
+ Mirabelle/Tools/mirabelle_try0.ML \
TPTP/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \
Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \
Library/Inner_Product.thy
--- 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")