# HG changeset patch
# User wenzelm
# Date 1193670823 -3600
# Node ID 6d4d26e878f4044f5e9f9c47068a1b6ae29ad34c
# Parent  7463251e72736cddcf11f703544826c714893e9e
added bool_ord;

diff -r 7463251e7273 -r 6d4d26e878f4 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Oct 29 16:13:41 2007 +0100
+++ b/src/Pure/library.ML	Mon Oct 29 16:13:43 2007 +0100
@@ -195,6 +195,7 @@
   val is_equal: order -> bool
   val rev_order: order -> order
   val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
+  val bool_ord: bool * bool -> order
   val int_ord: int * int -> order
   val string_ord: string * string -> order
   val fast_string_ord: string * string -> order
@@ -921,6 +922,10 @@
   else if rel (y, x) then GREATER
   else EQUAL;
 
+fun bool_ord (false, true) = LESS
+  | bool_ord (true, false) = GREATER
+  | bool_ord _ = EQUAL;
+
 val int_ord = Int.compare;
 val string_ord = String.compare;