# HG changeset patch
# User wenzelm
# Date 1120564460 -7200
# Node ID cc735c10b44d634cac55f7a92af266105ad617b1
# Parent  4ffc943c9c75b7941f02dfa3db284f831e0f909e
tuned;

diff -r 4ffc943c9c75 -r cc735c10b44d src/Pure/net.ML
--- a/src/Pure/net.ML	Mon Jul 04 20:20:50 2005 +0200
+++ b/src/Pure/net.ML	Tue Jul 05 13:54:20 2005 +0200
@@ -87,7 +87,7 @@
 *)
 fun insert ((keys,x), net, eq) =
   let fun ins1 ([], Leaf xs) =
-            if gen_mem eq (x,xs) then  raise INSERT  else Leaf(x::xs)
+            if member eq xs x then  raise INSERT  else Leaf(x::xs)
         | ins1 (keys, Leaf[]) = ins1 (keys, emptynet)   (*expand empty...*)
         | ins1 (CombK :: keys, Net{comb,var,alist}) =
             Net{comb=ins1(keys,comb), var=var, alist=alist}
@@ -124,7 +124,7 @@
   eq is the equality test for items. *)
 fun delete ((keys, x), net, eq) =
   let fun del1 ([], Leaf xs) =
-            if gen_mem eq (x,xs) then Leaf (gen_rem (eq o swap) (xs,x))
+            if member eq xs x then Leaf (remove eq x xs)
             else raise DELETE
         | del1 (keys, Leaf[]) = raise DELETE
         | del1 (CombK :: keys, Net{comb,var,alist}) =
@@ -232,11 +232,8 @@
 
 (** merge **)
 
-fun add eq (net, keys_x) =
-  insert (keys_x, net, eq) handle INSERT => net;
-
-fun merge (net1, net2, eq) =
-  Library.foldl (add eq) (net1, dest net2);
+fun add eq keys_x net = insert (keys_x, net, eq) handle INSERT => net;
+fun merge (net1, net2, eq) = fold (add eq) (dest net2) net1;
 
 
 end;