--- a/src/Pure/term.ML Wed Nov 13 10:41:50 1996 +0100
+++ b/src/Pure/term.ML Wed Nov 13 10:42:50 1996 +0100
@@ -322,6 +322,12 @@
fun mem_term (_, []) = false
| mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
+fun subset_term ([], ys) = true
+ | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
+
+fun eq_set_term (xs, ys) =
+ xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
+
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
fun union_term (xs, []) = xs
@@ -355,6 +361,12 @@
| union_sort ([], ys) = ys
| union_sort ((x :: xs), ys) = union_sort (xs, ins_sort (x, ys));
+fun subset_sort ([], ys) = true
+ | 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));
+
(*are two term lists alpha-convertible in corresponding elements?*)
fun aconvs ([],[]) = true
| aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)