tuned;
authorwenzelm
Tue, 05 Jul 2005 13:54:20 +0200
changeset 16686 cc735c10b44d
parent 16685 4ffc943c9c75
child 16687 51fa05ce0f32
tuned;
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;