# HG changeset patch
# User wenzelm
# Date 869586440 -7200
# Node ID 108d09eb3454225d772fe3690296601894199a04
# Parent  977d58464d7f3281c32102b0d3861d97c691a0e4
added dest and merge operations;

diff -r 977d58464d7f -r 108d09eb3454 src/Pure/net.ML
--- a/src/Pure/net.ML	Tue Jul 22 17:46:35 1997 +0200
+++ b/src/Pure/net.ML	Tue Jul 22 17:47:20 1997 +0200
@@ -28,6 +28,8 @@
   val match_term: 'a net -> term -> 'a list
   val key_of_term: term -> key list
   val unify_term: 'a net -> term -> 'a list
+  val dest: 'a net -> (key list * 'a) list
+  val merge: 'a net * 'a net * ('a*'a -> bool) -> 'a net
   end;
 
 
@@ -215,4 +217,26 @@
 fun unify_term net t = 
     extract_leaves (matching true t (net,[]));
 
+
+(** dest **)
+
+fun cons_fst x (xs, y) = (x :: xs, y);
+val cons_fsts = map o cons_fst;
+
+fun dest (Leaf xs) = map (pair []) xs
+  | dest (Net {comb, var, alist}) =
+      cons_fsts CombK (dest comb) @
+      cons_fsts VarK (dest var) @
+      flat (map (fn (a, net) => cons_fsts (AtomK a) (dest net)) alist);
+
+
+(** merge **)
+
+fun add eq (net, keys_x) =
+  insert (keys_x, net, eq) handle INSERT => net;
+
+fun merge (net1, net2, eq) =
+  foldl (add eq) (net1, dest net2);
+
+
 end;