--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 14 14:22:49 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 14 14:47:53 2010 +0200
@@ -492,7 +492,8 @@
|> snd
end
-val try_timeout = Time.fromSeconds 30
+val try_inner_timeout = Time.fromSeconds 5
+val try_outer_timeout = Time.fromSeconds 30
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
@@ -503,9 +504,9 @@
Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
-
- val trivial = Try.invoke_try (SOME try_timeout) pre
-
+ val trivial = TimeLimit.timeLimit try_outer_timeout
+ (Try.invoke_try (SOME try_inner_timeout)) pre
+ handle TimeLimit.TimeOut => false
fun apply_metis m1 m2 =
if metis_ft
then