Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sun, 05 Jan 2025 15:18:54 +0100
changeset 81729 560a069a537f
parent 81728 6e25f82056ad
child 81730 b836e9ac0cf3
tuned;
src/HOL/Tools/Nitpick/nitpick.ML file | annotate | diff | comparison | revisions
src/Pure/Tools/find_theorems.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle