--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Dec 19 13:43:21 2013 +0100
@@ -172,7 +172,7 @@
val is_problem_trivially_false : problem -> bool
val problems_equivalent : problem * problem -> bool
val solve_any_problem :
- bool -> bool -> Time.time option -> int -> int -> problem list -> outcome
+ bool -> bool -> Time.time -> int -> int -> problem list -> outcome
end;
structure Kodkod : KODKOD =
@@ -983,10 +983,7 @@
val fudge_ms = 250
fun milliseconds_until_deadline deadline =
- case deadline of
- NONE => ~1
- | SOME time =>
- Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) - fudge_ms)
+ Int.max (0, Time.toMilliseconds (Time.- (deadline, Time.now ())) - fudge_ms)
fun uncached_solve_any_problem overlord deadline max_threads max_solutions
problems =