src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
changeset 62826 eb94e570c1a4
parent 62735 23de054397e5
child 63692 1bc4bc2c9fd1
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -250,7 +250,7 @@
     1.4                * 0.001
     1.5                |> seconds
     1.6              val generous_slice_timeout =
     1.7 -              if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
     1.8 +              if mode = MaSh then one_day else slice_timeout + atp_timeout_slack
     1.9              val _ =
    1.10                if debug then
    1.11                  quote name ^ " slice #" ^ string_of_int (slice + 1) ^
    1.12 @@ -328,14 +328,14 @@
    1.13          val timer = Timer.startRealTimer ()
    1.14  
    1.15          fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) =
    1.16 -            let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in
    1.17 -              if Time.<= (time_left, Time.zeroTime) then
    1.18 +            let val time_left = timeout - Timer.checkRealTimer timer in
    1.19 +              if time_left <= Time.zeroTime then
    1.20                  result
    1.21                else
    1.22                  run_slice time_left cache slice
    1.23                  |> (fn (cache, (output, run_time, used_from, atp_proof, outcome),
    1.24                          format_type_enc) =>
    1.25 -                  (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome),
    1.26 +                  (cache, (output, run_time0 + run_time, used_from, atp_proof, outcome),
    1.27                     format_type_enc))
    1.28              end
    1.29            | maybe_run_slice _ result = result