# HG changeset patch
# User wenzelm
# Date 938605901 -7200
# Node ID f586d7995474c57a7e5a73ad3c1c97dd402fe1e2
# Parent  16347ef1d222a90167bb94e098c1b523848505bc
added rems_sort;

diff -r 16347ef1d222 -r f586d7995474 src/Pure/term.ML
--- 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)