# HG changeset patch
# User wenzelm
# Date 881239791 -3600
# Node ID b449831f03f47dcc112f1529aaee30c8c7ab3250
# Parent  e10acc395f0db42551df377cd9d4f7971b304ae5
added eq_set;

diff -r e10acc395f0d -r b449831f03f4 src/Pure/library.ML
--- 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);