--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 15 19:57:12 2012 +0100
@@ -68,7 +68,7 @@
{state, goal, subgoal, subgoal_count, facts} name =
let
val ctxt = Proof.context_of state
- val hard_timeout = Time.+ (timeout, timeout)
+ val hard_timeout = time_mult 2.0 (timeout |> the_default one_day)
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, hard_timeout)
val max_facts =
@@ -131,7 +131,7 @@
in (outcome_code, message) end
in
if mode = Auto_Try then
- let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
+ let val (outcome_code, message) = time_limit timeout go () in
(outcome_code,
state
|> outcome_code = someN