# HG changeset patch
# User desharna
# Date 1696238573 -7200
# Node ID 45867a453a3f1d862f388692b25cd09f2ce58b70
# Parent  a0f85118488cbfcd5a833ac512dbbcbaf4435be1
used standard Time.compare in Sledgehammer's preplay

diff -r a0f85118488c -r 45867a453a3f src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Sep 29 17:22:19 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Oct 02 11:22:53 2023 +0200
@@ -160,12 +160,10 @@
     if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"
   | string_of_play_outcome Play_Failed = "failed"
 
-fun play_outcome_ord (Played time1, Played time2) =
-    int_ord (apply2 Time.toMilliseconds (time1, time2))
+fun play_outcome_ord (Played time1, Played time2) = Time.compare (time1, time2)
   | play_outcome_ord (Played _, _) = LESS
   | play_outcome_ord (_, Played _) = GREATER
-  | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
-    int_ord (apply2 Time.toMilliseconds (time1, time2))
+  | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) = Time.compare (time1, time2)
   | play_outcome_ord (Play_Timed_Out _, _) = LESS
   | play_outcome_ord (_, Play_Timed_Out _) = GREATER
   | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL