changeset 4479 | 708d7c26db5b |
parent 4445 | de74b549f976 |
child 4496 | 16187138463d |
--- 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