fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER
authorpaulson
Wed, 01 Dec 1999 11:15:56 +0100
changeset 8043 0e4434d55df9
parent 8042 ecdedff41e67
child 8044 296b03b79505
fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER (for Moscow ML)
src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Nov 30 17:53:34 1999 +0100
+++ b/src/Pure/library.ML	Wed Dec 01 11:15:56 1999 +0100
@@ -202,7 +202,7 @@
   val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list
 
   (*orders*)
-  datatype order = EQUAL | GREATER | LESS
+  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