# HG changeset patch
# User haftmann
# Date 1135174716 -3600
# Node ID 5ea633c9bc057043029d334b6eb2384c222be7ac
# Parent  5ff0244e25e81f6caff4dca40b8ec4605b4ae769
added eq_ord

diff -r 5ff0244e25e8 -r 5ea633c9bc05 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Dec 21 15:18:17 2005 +0100
+++ b/src/Pure/library.ML	Wed Dec 21 15:18:36 2005 +0100
@@ -223,6 +223,7 @@
   (*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
@@ -1079,6 +1080,11 @@
   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;