# HG changeset patch # User wenzelm # Date 1350661941 -7200 # Node ID 3e7522664453c41da3ffcb5f43c294e9ec6d3e58 # Parent d1ecb3554b2546b83657360588290cecbcd78b9a made SML/NJ happy; diff -r d1ecb3554b25 -r 3e7522664453 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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) ();