--- a/src/Pure/item_net.ML Sun Aug 16 14:48:37 2015 +0200
+++ b/src/Pure/item_net.ML Sun Aug 16 15:36:06 2015 +0200
@@ -14,6 +14,7 @@
val retrieve: 'a T -> term -> 'a list
val retrieve_matching: 'a T -> term -> 'a list
val member: 'a T -> 'a -> bool
+ val lookup: 'a T -> 'a -> 'a list
val merge: 'a T * 'a T -> 'a T
val remove: 'a -> 'a T -> 'a T
val update: 'a -> 'a T -> 'a T
@@ -50,6 +51,12 @@
[] => Library.member eq content x
| t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));
+fun lookup (Items {eq, index, content, net, ...}) x =
+ (case index x of
+ [] => content
+ | t :: _ => map #2 (Net.unify_term net t))
+ |> filter (fn y => eq (x, y));
+
fun cons x (Items {eq, index, content, next, net}) =
mk_items eq index (x :: content) (next - 1)
(fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);