1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 13:43:46 2010 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 13:48:24 2010 +0100
     1.3 @@ -419,7 +419,9 @@
     1.4      val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
     1.5      val dir = AList.lookup (op =) args keepK
     1.6      val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
     1.7 -    val hard_timeout = SOME timeout (* always use a hard timeout *)
     1.8 +    (* always use a hard timeout, but give some slack so that the automatic
     1.9 +       minimizer has a chance to do its magic *)
    1.10 +    val hard_timeout = SOME (2 * timeout)
    1.11      val (msg, result) =
    1.12        run_sh prover_name prover type_sys hard_timeout timeout dir st
    1.13    in