src/Pure/item_net.ML
changeset 59058 a78612c67ec0
parent 55741 b969263fcf02
child 60946 46ec72073dc1
--- a/src/Pure/item_net.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/Pure/item_net.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -64,7 +64,7 @@
 fun remove x (items as Items {eq, index, content, next, net}) =
   if member items x then
     mk_items eq index (Library.remove eq x content) next
-      (fold (fn t => Net.delete_term_safe (eq o pairself #2) (t, (0, x))) (index x) net)
+      (fold (fn t => Net.delete_term_safe (eq o apply2 #2) (t, (0, x))) (index x) net)
   else items;
 
 fun update x items = cons x (remove x items);