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);