# HG changeset patch
# User wenzelm
# Date 1353088186 -3600
# Node ID 3d89c38408cd72170e74d3c794d2817e4e6acd00
# Parent  a3bede207a0488a088a080c3485ce795aa94ef5a# Parent  5e01e32dadbea9273ff6959db3383db56f8ce537
merged

diff -r a3bede207a04 -r 3d89c38408cd src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Nov 16 14:46:23 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Nov 16 18:49:46 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