src/Pure/term.ML

   val mem_sort: sort * class list list -> bool
   val subset_sort: sort list * class list list -> bool
   val eq_set_sort: sort list * sort list -> bool
   val ins_sort: sort * class list list -> class list list
   val union_sort: sort list * sort list -> sort list
+  val rems_sort: sort list * sort list -> sort list
   val aconv: term * term -> bool
   val aconvs: term list * term list -> bool
   val mem_term: term * term list -> bool
   val subset_term: term list * term list -> bool
   val eq_set_term: term list * term list -> bool

   | subset_sort (x :: xs, ys) = mem_sort (x, ys) andalso subset_sort(xs, ys);
 
 fun eq_set_sort (xs, ys) =
     xs = ys orelse (subset_sort (xs, ys) andalso subset_sort (ys, xs));
 
+val rems_sort = gen_rems eq_sort;
+
 (*are two term lists alpha-convertible in corresponding elements?*)
 fun aconvs ([],[]) = true
   | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
   | aconvs _ = false;