author | wenzelm |
Fri, 19 Oct 2012 17:52:21 +0200 | |
changeset 49936 | 3e7522664453 |
parent 49935 | d1ecb3554b25 |
child 49937 | 463cdbfba8c7 |
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML | file | annotate | diff | comparison | revisions |
--- 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) ();