# HG changeset patch
# User paulson
# Date 1051353497 -7200
# Node ID 761af5c2fd591964e7dd5029454fada337307b2d
# Parent  09f6f2fefb255e3a516f40775bcc541fe9a90333
catches exception DELETE

diff -r 09f6f2fefb25 -r 761af5c2fd59 src/Pure/tactic.ML
--- 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;