diff -r 3d9d2ef0cd3b -r 927a31ba4346 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Jun 14 12:26:06 1996 +0200
+++ b/src/Pure/tactic.ML	Fri Jun 14 12:27:11 1996 +0200
@@ -46,6 +46,9 @@
   val insert_tagged_brl:  ('a*(bool*thm)) * 
                     (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
                     ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
+  val delete_tagged_brl:  (bool*thm) * 
+                    ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) ->
+                    (int*(bool*thm))Net.net * (int*(bool*thm))Net.net
   val is_fact: thm -> bool
   val lessb: (bool * thm) * (bool * thm) -> bool
   val lift_inst_rule: thm * int * (string*string)list * thm -> thm
@@ -315,6 +318,20 @@
 fun build_netpair netpair brls = 
     foldr insert_tagged_brl (taglist 1 brls, netpair);
 
+(*delete one kbrl from the pair of nets;
+  we don't know the value of k, so we use 0 and ignore it in the comparison*)
+local
+  fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th')
+in
+fun delete_tagged_brl (brl as (eres,th), (inet,enet)) =
+    if eres then 
+	case prems_of th of
+	    prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
+	  | [] => error"delete_brl: elimination rule with no premises"
+    else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
+end;
+
+
 (*biresolution using a pair of nets rather than rules*)
 fun biresolution_from_nets_tac match (inet,enet) =
   SUBGOAL