src/Pure/library.ML
changeset 2182 29e56f003599
parent 2175 21fde76bc742
child 2196 1b36ebc70487
     1.1 --- a/src/Pure/library.ML	Wed Nov 13 10:41:50 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Nov 13 10:42:50 1996 +0100
     1.3 @@ -492,24 +492,12 @@
     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 -fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
     1.8 -
     1.9 -
    1.10 -(*eq_set*)
    1.11 -
    1.12 -fun eq_set (xs, ys) =
    1.13 -  xs = ys orelse (xs subset ys andalso ys subset xs);
    1.14 -
    1.15 -(*eq_set, optimized version for ints*)
    1.16 -
    1.17 -fun eq_set_int ((xs:int list), ys) =
    1.18 -  xs = ys orelse (xs subset_int ys andalso ys subset_int xs);
    1.19 -
    1.20 -(*eq_set, optimized version for strings*)
    1.21 -
    1.22 +(*set equality for strings*)
    1.23  fun eq_set_string ((xs:string list), ys) =
    1.24    xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
    1.25  
    1.26 +fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
    1.27 +
    1.28  
    1.29  (*removing an element from a list WITHOUT duplicates*)
    1.30  fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
    1.31 @@ -886,8 +874,9 @@
    1.32  fun transitive_closure [] = []
    1.33    | transitive_closure ((x, ys)::ps) =
    1.34        let val qs = transitive_closure ps
    1.35 -          val zs = foldl (fn (zs, y) => assocs qs y union zs) (ys, ys)
    1.36 -          fun step(u, us) = (u, if x mem us then zs union us else us)
    1.37 +          val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
    1.38 +          fun step(u, us) = (u, if x mem_string us then zs union_string us 
    1.39 +				else us)
    1.40        in (x, zs) :: map step qs end;
    1.41  
    1.42