--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Wed Nov 26 20:05:34 2014 +0100
@@ -149,11 +149,11 @@
| string_of_play_outcome Play_Failed = "failed"
fun play_outcome_ord (Played time1, Played time2) =
- int_ord (pairself Time.toMilliseconds (time1, time2))
+ int_ord (apply2 Time.toMilliseconds (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 (pairself Time.toMilliseconds (time1, time2))
+ int_ord (apply2 Time.toMilliseconds (time1, time2))
| play_outcome_ord (Play_Timed_Out _, _) = LESS
| play_outcome_ord (_, Play_Timed_Out _) = GREATER
| play_outcome_ord (Play_Failed, Play_Failed) = EQUAL