--- 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