# HG changeset patch
# User wenzelm
# Date 1152040972 -7200
# Node ID f14c03e08e22270e7209aa4ff023383696456080
# Parent  bcadd6e7739cfb94fa81c1d7e7378426a36dedb6
added content;

diff -r bcadd6e7739c -r f14c03e08e22 src/Pure/net.ML
--- 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;