src/HOL/Tools/Sledgehammer/sledgehammer.ML

       | SOME SMT_Failure.Out_Of_Memory => true
       | SOME _ => true
     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
       end
     else