1.1 --- a/src/Pure/General/ord_list.ML	Mon Feb 26 23:18:28 2007 +0100
     1.2 +++ b/src/Pure/General/ord_list.ML	Mon Feb 26 23:18:29 2007 +0100
     1.3 @@ -12,7 +12,6 @@
     1.4    val insert: ('a * 'a -> order) -> 'a -> 'a list -> 'a list
     1.5    val remove: ('b * 'a -> order) -> 'b -> 'a list -> 'a list
     1.6    val subset: ('b * 'a -> order) -> 'b list * 'a list -> bool
     1.7 -  val eq_set: ('b * 'a -> order) -> 'b list * 'a list -> bool
     1.8    val union: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
     1.9    val inter: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
    1.10    val subtract: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
    1.11 @@ -65,8 +64,6 @@
    1.12            | GREATER => sub lst1 ys);
    1.13    in sub list1 list2 end;
    1.14  
    1.15 -fun eq_set ord lists = (list_ord ord lists = EQUAL);
    1.16 -
    1.17  
    1.18  (* algebraic operations *)
    1.19  

     2.1 --- a/src/Pure/sorts.ML	Mon Feb 26 23:18:28 2007 +0100
     2.2 +++ b/src/Pure/sorts.ML	Mon Feb 26 23:18:29 2007 +0100
     2.3 @@ -15,7 +15,6 @@
     2.4  
     2.5  signature SORTS =
     2.6  sig
     2.7 -  val eq_set: sort list * sort list -> bool
     2.8    val union: sort list -> sort list -> sort list
     2.9    val subtract: sort list -> sort list -> sort list
    2.10    val remove_sort: sort -> sort list -> sort list
    2.11 @@ -66,7 +65,6 @@
    2.12  
    2.13  (** ordered lists of sorts **)
    2.14  
    2.15 -val eq_set = OrdList.eq_set Term.sort_ord;
    2.16  val op union = OrdList.union Term.sort_ord;
    2.17  val subtract = OrdList.subtract Term.sort_ord;
    2.18