diff -r 3897af72c731 -r 285aea0c153c src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 22:15:39 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 23:31:22 2010 +0100
@@ -531,8 +531,7 @@
     |> snd
   end
 
-val try_inner_timeout = seconds 5.0
-val try_outer_timeout = seconds 30.0
+val try_timeout = seconds 5.0
 
 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
   let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
@@ -544,10 +543,8 @@
         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 =
-       TimeLimit.timeLimit try_outer_timeout
-                                   (Try.invoke_try (SOME try_inner_timeout)) pre
-                    handle TimeLimit.TimeOut => false
+      val trivial = Try.invoke_try (SOME try_timeout) pre
+        handle TimeLimit.TimeOut => false
       fun apply_reconstructor m1 m2 =
         if metis_ft
         then