# HG changeset patch
# User blanchet
# Date 1309673714 -7200
# Node ID 5742b288bb8671f8c9f413d12843441489178c10
# Parent  3f1a44c2d64554f5a00e79dd84344cd7389df229
make SML/NJ happy

diff -r 3f1a44c2d645 -r 5742b288bb86 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Jul 02 22:55:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 03 08:15:14 2011 +0200
@@ -627,7 +627,8 @@
                         else
                           I))
                    * 0.001) |> seconds
-                val generous_slice_timeout = slice_timeout + atp_timeout_slack
+                val generous_slice_timeout =
+                  Time.+ (slice_timeout, atp_timeout_slack)
                 val _ =
                   if debug then
                     quote name ^ " slice #" ^ string_of_int (slice + 1) ^