src/Pure/library.ML

   val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list
 
   (*orders*)
   val rev_order: order -> order
   val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
+  val eq_ord: ('a -> order) -> 'a -> bool
   val int_ord: int * int -> order
   val string_ord: string * string -> order
   val fast_string_ord: string * string -> order
   val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
   val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order

 (*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
   else EQUAL;
+
+fun eq_ord ord xy =
+  case ord xy
+   of EQUAL => true
+    | _ => false;
 
 val int_ord = Int.compare;
 val string_ord = String.compare;
 
 fun fast_string_ord (s1, s2) =