catches exception DELETE

--- a/src/Pure/tactic.ML	Fri Apr 25 15:17:36 2003 +0200
+++ b/src/Pure/tactic.ML	Sat Apr 26 12:38:17 2003 +0200
@@ -418,11 +418,12 @@
   fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
 in
 fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
-  if eres then
+  (if eres then
     (case try Thm.major_prem_of th of
       Some prem => (inet, Net.delete_term ((prem, ((), brl)), enet, eq_kbrl))
     | None => (inet, enet))  (*no major premise: ignore*)
-  else (Net.delete_term ((Thm.concl_of th, ((), brl)), inet, eq_kbrl), enet);
+  else (Net.delete_term ((Thm.concl_of th, ((), brl)), inet, eq_kbrl), enet))
+  handle Net.DELETE => (inet,enet);
 end;