# HG changeset patch
# User wenzelm
# Date 1172528309 -3600
# Node ID ddb91c9eb0fc816e299a97a03c4d30d65991d623
# Parent  a9f56907eab7b52f4ac2fd7b4d8fe25dec4066e6
removed obsolete eq_set;

diff -r a9f56907eab7 -r ddb91c9eb0fc src/Pure/General/ord_list.ML
--- 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 *)
 
diff -r a9f56907eab7 -r ddb91c9eb0fc src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Feb 26 23:18:28 2007 +0100
+++ b/src/Pure/sorts.ML	Mon Feb 26 23:18:29 2007 +0100
@@ -15,7 +15,6 @@
 
 signature SORTS =
 sig
-  val eq_set: sort list * sort list -> bool
   val union: sort list -> sort list -> sort list
   val subtract: sort list -> sort list -> sort list
   val remove_sort: sort -> sort list -> sort list
@@ -66,7 +65,6 @@
 
 (** ordered lists of sorts **)
 
-val eq_set = OrdList.eq_set Term.sort_ord;
 val op union = OrdList.union Term.sort_ord;
 val subtract = OrdList.subtract Term.sort_ord;