added eq_ord
authorhaftmann
Wed Dec 21 15:18:36 2005 +0100 (2005-12-21)
changeset 184525ea633c9bc05
parent 18451 5ff0244e25e8
child 18453 2b2fbc32550e
added eq_ord
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Dec 21 15:18:17 2005 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Dec 21 15:18:36 2005 +0100
     1.3 @@ -223,6 +223,7 @@
     1.4    (*orders*)
     1.5    val rev_order: order -> order
     1.6    val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
     1.7 +  val eq_ord: ('a -> order) -> 'a -> bool
     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 @@ -1079,6 +1080,11 @@
    1.12    else if rel (y, x) then GREATER
    1.13    else EQUAL;
    1.14  
    1.15 +fun eq_ord ord xy =
    1.16 +  case ord xy
    1.17 +   of EQUAL => true
    1.18 +    | _ => false;
    1.19 +
    1.20  val int_ord = Int.compare;
    1.21  val string_ord = String.compare;
    1.22