changeset 49936 | 3e7522664453 |
parent 49921 | 073d69478207 |
child 49981 | e12b4e9794fd |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Oct 19 12:08:13 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Oct 19 17:52:21 2012 +0200 @@ -819,7 +819,7 @@ val t1 = try_metis s1 s0 () val t2 = try_metis s2 (SOME s1) () val timeout = - t1 + t2 |> Time.toReal |> curry Real.* merge_timeout_slack + Time.+ (t1, t2) |> Time.toReal |> curry Real.* merge_timeout_slack |> Time.fromReal in (TimeLimit.timeLimit timeout (try_metis s12 s0) ();