diff -r 9c2b4728641d -r 29e56f003599 src/Pure/term.ML
--- 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)