# HG changeset patch
# User wenzelm
# Date 1353081596 -3600
# Node ID 5e01e32dadbea9273ff6959db3383db56f8ce537
# Parent  94d7dfa9f40436ff8e47019de3ad1cb7c3392360
made SML/NJ happy;

diff -r 94d7dfa9f404 -r 5e01e32dadbe src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Nov 16 11:34:34 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Nov 16 16:59:56 2012 +0100
@@ -814,8 +814,8 @@
       end
     val sum_up_time =
       Vector.foldl
-        ((fn (SOME t, (b, s)) => (b, t + s)
-           | (NONE, (_, s)) => (true, preplay_timeout + s)) o apfst Lazy.force)
+        ((fn (SOME t, (b, s)) => (b, Time.+ (t, s))
+           | (NONE, (_, s)) => (true, Time.+ (preplay_timeout, s))) o apfst Lazy.force)
         (false, seconds 0.0)
 
     (* Metis Preplaying *)
@@ -858,7 +858,7 @@
           let
             val s12 = merge s1 s2
             val timeout =
-              t1 + t2 |> Time.toReal |> curry Real.* merge_timeout_slack
+              Time.+ (t1, t2) |> Time.toReal |> curry Real.* merge_timeout_slack
                       |> Time.fromReal
           in
             case try_metis timeout s12 () of