# HG changeset patch
# User wenzelm
# Date 1736086734 -3600
# Node ID 560a069a537f0dc38972b1a0d4874102f0e4b572
# Parent  6e25f82056ad82d6c8e3154be8840d05ec329a3b
tuned;

diff -r 6e25f82056ad -r 560a069a537f src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Jan 05 15:18:30 2025 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Jan 05 15:18:54 2025 +0100
@@ -230,7 +230,7 @@
 
     fun check_deadline () =
       let val t = Time.now () in
-        if Time.compare (t, deadline) <> LESS
+        if t >= deadline
         then raise Timeout.TIMEOUT (t - time_start)
         else ()
       end
diff -r 6e25f82056ad -r 560a069a537f src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sun Jan 05 15:18:30 2025 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sun Jan 05 15:18:54 2025 +0100
@@ -345,7 +345,7 @@
         (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
       | ord => ord)
     | ord => ord)
-  | ord => ord) <> GREATER;
+  | ord => ord) |> is_less_equal;
 
 fun rem_cdups nicer xs =
   let