# HG changeset patch
# User wenzelm
# Date 1089963364 -7200
# Node ID 0dbbab9f77fe1a2f65c825b870ff16b1236f53b5
# Parent  e02f678887bb4497df2a7d1759b928a46076b632
int_ord = Int.compare, string_ord = String.compare;

diff -r e02f678887bb -r 0dbbab9f77fe src/Pure/library.ML
--- 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')) =