1.1 --- a/src/Pure/library.ML	Thu Dec 04 13:49:27 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Dec 04 13:49:51 1997 +0100
     1.3 @@ -514,6 +514,10 @@
     1.4  fun ([]:string list) subset_string ys = true
     1.5    | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
     1.6  
     1.7 +(*set equality*)
     1.8 +fun eq_set (xs, ys) =
     1.9 +  xs = ys orelse (xs subset ys andalso ys subset xs);
    1.10 +
    1.11  (*set equality for strings*)
    1.12  fun eq_set_string ((xs:string list), ys) =
    1.13    xs = ys orelse (xs subset_string ys andalso ys subset_string xs);