# HG changeset patch
# User blanchet
# Date 1289376187 -3600
# Node ID 2269544b645730911fc7df8fe6db1df729a13cc4
# Parent  2878445aa7d54a28a41d19d498610460360ab65f
make SML/NJ happy

diff -r 2878445aa7d5 -r 2269544b6457 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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