# HG changeset patch
# User lammich <lammich@in.tum.de>
# Date 1380207144 -7200
# Node ID 54874871aa066bcf9e7099ee074f1d46389031f4
# Parent  36cf426cb1c67d04ef8108f1948d35cb91a2aed7
Added Item_Net.retrieve_matching

diff -r 36cf426cb1c6 -r 54874871aa06 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 *)