int_ord = Int.compare, string_ord = String.compare;

--- a/src/Pure/library.ML	Thu Jul 15 15:47:39 2004 +0200
+++ b/src/Pure/library.ML	Fri Jul 16 09:36:04 2004 +0200
@@ -1111,17 +1111,8 @@
   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
-  else GREATER;
+val int_ord = Int.compare;
+val string_ord = String.compare;
 
 (*lexicographic product*)
 fun prod_ord a_ord b_ord ((x, y), (x', y')) =