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