# HG changeset patch
# User blanchet
# Date 1357421491 -3600
# Node ID 82dee320d34097ce7dfee88fa81a635c2cf8e77f
# Parent  c056718eb6879acc8de3dcaa76d47278d8978831
increased hard timeout -- minimization can take time

diff -r c056718eb687 -r 82dee320d340 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Jan 05 22:31:30 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Jan 05 22:31:31 2013 +0100
@@ -68,7 +68,7 @@
                   {state, goal, subgoal, subgoal_count, facts} name =
   let
     val ctxt = Proof.context_of state
-    val hard_timeout = time_mult 2.0 (timeout |> the_default one_day)
+    val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, hard_timeout)
     val max_facts =