src/HOL/Tools/Nitpick/nitpick.ML
changeset 62826 eb94e570c1a4
parent 62519 a564458f94db
child 63693 5b02f7757a4c
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -251,7 +251,7 @@
     1.4      fun check_deadline () =
     1.5        let val t = Time.now () in
     1.6          if Time.compare (t, deadline) <> LESS
     1.7 -        then raise Timeout.TIMEOUT (Time.- (t, time_start))
     1.8 +        then raise Timeout.TIMEOUT (t - time_start)
     1.9          else ()
    1.10        end
    1.11  
    1.12 @@ -540,7 +540,7 @@
    1.13          val bit_width = if bits = 0 then 16 else bits + 1
    1.14          val delay =
    1.15            if unsound then
    1.16 -            unsound_delay_for_timeout (Time.- (deadline, Time.now ()))
    1.17 +            unsound_delay_for_timeout (deadline - Time.now ())
    1.18            else
    1.19              0
    1.20          val settings = [("solver", commas_quote kodkod_sat_solver),
    1.21 @@ -986,9 +986,9 @@
    1.22      else
    1.23        let
    1.24          val unknown_outcome = (unknownN, [])
    1.25 -        val deadline = Time.+ (Time.now (), timeout)
    1.26 +        val deadline = Time.now () + timeout
    1.27          val outcome as (outcome_code, _) =
    1.28 -          Timeout.apply (Time.+ (timeout, timeout_bonus))
    1.29 +          Timeout.apply (timeout + timeout_bonus)
    1.30                (pick_them_nits_in_term deadline state params mode i n step subst
    1.31                                        def_assm_ts nondef_assm_ts) orig_t
    1.32            handle TOO_LARGE (_, details) =>