# HG changeset patch
# User wenzelm
# Date 1136934665 -3600
# Node ID 612dcdd9c03dc8b2e8f4565de40a6e4909face33
# Parent  8911c5a8b078dad8896178a5fc4eb08e1b0e181d
tuned;

diff -r 8911c5a8b078 -r 612dcdd9c03d src/Pure/Isar/net_rules.ML
--- a/src/Pure/Isar/net_rules.ML	Wed Jan 11 00:11:02 2006 +0100
+++ b/src/Pure/Isar/net_rules.ML	Wed Jan 11 00:11:05 2006 +0100
@@ -54,8 +54,8 @@
   in fold_rev add rules (init eq index) end;
 
 fun delete rule (rs as Rules {eq, index, rules, next, net}) =
-  if not (Library.gen_mem eq (rule, rules)) then rs
-  else mk_rules eq index (Library.gen_rem eq (rules, rule)) next
+  if not (member eq rules rule) then rs
+  else mk_rules eq index (remove eq rule rules) next
     (Net.delete_term (eq o pairself #2) (index rule, (0, rule)) net);
 
 fun insert rule rs = add rule (delete rule rs);    (*ensure that new rule gets precedence*)