src/Pure/item_net.ML

--- a/src/Pure/item_net.ML	Thu Sep 26 13:37:33 2013 +0200
+++ b/src/Pure/item_net.ML	Thu Sep 26 16:52:24 2013 +0200
@@ -12,6 +12,7 @@
   val content: 'a T -> 'a list
   val length: 'a T -> int
   val retrieve: 'a T -> term -> 'a list
+  val retrieve_matching: 'a T -> term -> 'a list
   val member: 'a T -> 'a -> bool
   val merge: 'a T * 'a T -> 'a T
   val remove: 'a -> 'a T -> 'a T
@@ -39,6 +40,7 @@
 fun content (Items {content, ...}) = content;
 fun length items = List.length (content items);
 fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
+fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net;
 
 
 (* standard operations *)