# HG changeset patch
# User wenzelm
# Date 1258404992 -3600
# Node ID f15c9ded96761491a9b4b2e34aa7ea1735a5de61
# Parent  d15212c7501c94acdcfd1c63ba63638bdbcbb079
member/cons: slightly more correct treatment of multi-index, notably empty one;

diff -r d15212c7501c -r f15c9ded9676 src/Pure/item_net.ML
--- a/src/Pure/item_net.ML	Mon Nov 16 20:23:02 2009 +0100
+++ b/src/Pure/item_net.ML	Mon Nov 16 21:56:32 2009 +0100
@@ -40,12 +40,14 @@
 
 (* standard operations *)
 
-fun member (Items {eq, index, net, ...}) x =
-  exists (fn t => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t)) (index x);
+fun member (Items {eq, index, content, net, ...}) x =
+  (case index x of
+    [] => Library.member eq content x
+  | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));
 
 fun cons x (Items {eq, index, content, next, net}) =
   mk_items eq index (x :: content) (next - 1)
-    (fold (fn t => Net.insert_term_safe (eq o pairself #2) (t, (next, x))) (index x) net);
+    (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
 
 
 fun merge (items1, Items {content = content2, ...}) =