src/Pure/library.ML
changeset 15051 0dbbab9f77fe
parent 15035 8c57751cd43f
child 15060 7b4abcfae4e1
     1.1 --- a/src/Pure/library.ML	Thu Jul 15 15:47:39 2004 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Jul 16 09:36:04 2004 +0200
     1.3 @@ -1111,17 +1111,8 @@
     1.4    else if rel (y, x) then GREATER
     1.5    else EQUAL;
     1.6  
     1.7 -(*Better to use Int.compare*)
     1.8 -fun int_ord (i, j: int) =
     1.9 -  if i < j then LESS
    1.10 -  else if i = j then EQUAL
    1.11 -  else GREATER;
    1.12 -
    1.13 -(*Better to use String.compare*)
    1.14 -fun string_ord (a, b: string) =
    1.15 -  if a < b then LESS
    1.16 -  else if a = b then EQUAL
    1.17 -  else GREATER;
    1.18 +val int_ord = Int.compare;
    1.19 +val string_ord = String.compare;
    1.20  
    1.21  (*lexicographic product*)
    1.22  fun prod_ord a_ord b_ord ((x, y), (x', y')) =