added eq_set;

--- a/src/Pure/library.ML	Thu Dec 04 13:49:27 1997 +0100
+++ b/src/Pure/library.ML	Thu Dec 04 13:49:51 1997 +0100
@@ -514,6 +514,10 @@
 fun ([]:string list) subset_string ys = true
   | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
 
+(*set equality*)
+fun eq_set (xs, ys) =
+  xs = ys orelse (xs subset ys andalso ys subset xs);
+
 (*set equality for strings*)
 fun eq_set_string ((xs:string list), ys) =
   xs = ys orelse (xs subset_string ys andalso ys subset_string xs);