1.1 --- a/src/Pure/library.ML	Mon Oct 29 16:13:41 2007 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Oct 29 16:13:43 2007 +0100
     1.3 @@ -195,6 +195,7 @@
     1.4    val is_equal: order -> bool
     1.5    val rev_order: order -> order
     1.6    val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
     1.7 +  val bool_ord: bool * bool -> order
     1.8    val int_ord: int * int -> order
     1.9    val string_ord: string * string -> order
    1.10    val fast_string_ord: string * string -> order
    1.11 @@ -921,6 +922,10 @@
    1.12    else if rel (y, x) then GREATER
    1.13    else EQUAL;
    1.14  
    1.15 +fun bool_ord (false, true) = LESS
    1.16 +  | bool_ord (true, false) = GREATER
    1.17 +  | bool_ord _ = EQUAL;
    1.18 +
    1.19  val int_ord = Int.compare;
    1.20  val string_ord = String.compare;
    1.21