--- a/src/Pure/library.ML Wed Mar 17 14:00:45 2004 +0100
+++ b/src/Pure/library.ML Fri Mar 19 10:42:38 2004 +0100
@@ -228,7 +228,6 @@
val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list
(*orders*)
- datatype order = LESS | EQUAL | GREATER
val rev_order: order -> order
val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
val int_ord: int * int -> order
@@ -1073,8 +1072,6 @@
(** orders **)
-datatype order = LESS | EQUAL | GREATER;
-
fun rev_order LESS = GREATER
| rev_order EQUAL = EQUAL
| rev_order GREATER = LESS;
@@ -1085,11 +1082,13 @@
else if rel (y, x) then GREATER
else EQUAL;
+(*Better to use Int.compare*)
fun int_ord (i, j: int) =
if i < j then LESS
else if i = j then EQUAL
else GREATER;
+(*Better to use String.compare*)
fun string_ord (a, b: string) =
if a < b then LESS
else if a = b then EQUAL