# HG changeset patch
# User wenzelm
# Date 882962454 -3600
# Node ID 708d7c26db5b9f7970a5e2b2e435784dbd8259b0
# Parent  9c5a0eef74ff6c379c11e650c5c91b1669bba22c
improved comment;

diff -r 9c5a0eef74ff -r 708d7c26db5b 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