--- a/src/Pure/General/ord_list.ML Mon Feb 26 23:18:28 2007 +0100
+++ b/src/Pure/General/ord_list.ML Mon Feb 26 23:18:29 2007 +0100
@@ -12,7 +12,6 @@
val insert: ('a * 'a -> order) -> 'a -> 'a list -> 'a list
val remove: ('b * 'a -> order) -> 'b -> 'a list -> 'a list
val subset: ('b * 'a -> order) -> 'b list * 'a list -> bool
- val eq_set: ('b * 'a -> order) -> 'b list * 'a list -> bool
val union: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
val inter: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
val subtract: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
@@ -65,8 +64,6 @@
| GREATER => sub lst1 ys);
in sub list1 list2 end;
-fun eq_set ord lists = (list_ord ord lists = EQUAL);
-
(* algebraic operations *)