made SML/NJ happy;
authorwenzelm
Fri, 19 Oct 2012 17:52:21 +0200
changeset 49936 3e7522664453
parent 49935 d1ecb3554b25
child 49937 463cdbfba8c7
made SML/NJ happy;
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) ();