diff -r 22e001795641 -r 49b05b9ead33 src/HOL/Mirabelle/Tools/mirabelle_try0.ML
--- 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")