src/Pure/library.ML

--- a/src/Pure/library.ML	Wed Dec 24 10:42:27 1997 +0100
+++ b/src/Pure/library.ML	Wed Dec 24 12:20:54 1997 +0100
@@ -729,6 +729,7 @@
   | rev_order EQUAL = EQUAL
   | rev_order GREATER = LESS;
 
+(*assume rel is a linear strict order*)
 fun make_ord rel (x, y) =
   if rel (x, y) then LESS
   else if rel (y, x) then GREATER