# HG changeset patch
# User paulson
# Date 944043356 -3600
# Node ID 0e4434d55df9e6dbf08f468a62c045800f032e95
# Parent  ecdedff41e67169758090d820b103b73e265de7b
fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER
(for Moscow ML)

diff -r ecdedff41e67 -r 0e4434d55df9 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