added content;

--- a/src/Pure/net.ML	Tue Jul 04 21:22:51 2006 +0200
+++ b/src/Pure/net.ML	Tue Jul 04 21:22:52 2006 +0200
@@ -32,6 +32,7 @@
   val entries: 'a net -> 'a list
   val subtract: ('b * 'a -> bool) -> 'a net -> 'b net -> 'b list
   val merge: ('a * 'a -> bool) -> 'a net * 'a net -> 'a net
+  val content: 'a net -> 'a list
 end;
 
 structure Net: NET =
@@ -240,4 +241,6 @@
 
 fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1;
 
+fun content net = map #2 (dest net);
+
 end;