# HG changeset patch
# User blanchet
# Date 1459159547 -7200
# Node ID 03b995c21878fe97465e7c103ab9eece5a7d2e50
# Parent  23de054397e50876f0ebc6e35fe4cdcb1bf77ed1
a more generous hard timeout

diff -r 23de054397e5 -r 03b995c21878 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -113,7 +113,7 @@
   let
     val ctxt = Proof.context_of state
 
-    val hard_timeout = time_mult 3.0 timeout
+    val hard_timeout = time_mult 5.0 timeout
     val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
     val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
     val num_facts = length facts |> not only ? Integer.min max_facts