author | blanchet |
Sun, 03 Jul 2011 08:15:14 +0200 | |
changeset 43655 | 5742b288bb86 |
parent 43654 | 3f1a44c2d645 |
child 43656 | 9ece73262746 |
--- 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) ^