--- a/src/Pure/term.ML Wed Sep 29 13:51:23 1999 +0200
+++ b/src/Pure/term.ML Wed Sep 29 13:51:41 1999 +0200
@@ -100,6 +100,7 @@
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
@@ -555,6 +556,8 @@
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)