# HG changeset patch
# User haftmann
# Date 1147162058 -7200
# Node ID 7b07dac44e096041292903feb132b1a53e54fcc7
# Parent  2042422ac7d8d4f1b67071dd1c4e26f4a799d7a6
removed superfluous eq_ord

diff -r 2042422ac7d8 -r 7b07dac44e09 src/Pure/General/name_mangler.ML
--- a/src/Pure/General/name_mangler.ML	Tue May 09 09:18:05 2006 +0200
+++ b/src/Pure/General/name_mangler.ML	Tue May 09 10:07:38 2006 +0200
@@ -136,7 +136,7 @@
 
 fun merge ((tab_f_1, tab_r_1), (tab_f_2, tab_r_2)) =
   (Srctab.merge (op = : string * string -> bool) (tab_f_1, tab_f_2),
-   Symtab.merge (eq_ord ord) (tab_r_1, tab_r_2));
+   Symtab.merge (is_equal o ord) (tab_r_1, tab_r_2));
 
 fun dest (tab_f, _) = Srctab.dest tab_f;
 
diff -r 2042422ac7d8 -r 7b07dac44e09 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue May 09 09:18:05 2006 +0200
+++ b/src/Pure/library.ML	Tue May 09 10:07:38 2006 +0200
@@ -4,8 +4,7 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Basic library: functions, options, pairs, booleans, lists, integers,
-strings, lists as sets, association lists, generic
-tables, balanced trees, orders, current directory, misc.
+strings, lists as sets, balanced trees, orders, current directory, misc.
 *)
 
 infix 1 |> |-> ||> ||>> |>> |>>> #> #->;
@@ -249,7 +248,6 @@
   val is_equal: order -> bool
   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