--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Nov 09 16:18:40 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Nov 10 09:03:07 2010 +0100
@@ -449,7 +449,7 @@
val timeout = Time.- (timeout, Timer.checkRealTimer timer)
in
if too_many_facts_perhaps andalso iter < smt_max_iter andalso
- not (null facts) andalso timeout > Time.zeroTime then
+ not (null facts) andalso Time.> (timeout, Time.zeroTime) then
let val facts = take (length facts div smt_iter_fact_divisor) facts in
smt_filter_loop (iter + 1) outcome0 msecs_so_far remote timeout state
facts i