# HG changeset patch
# User paulson
# Date 858763479 -3600
# Node ID a318f7f3a65cc6a9e4793abe9d658d3b6437ec5b
# Parent  cc4c816dafdc58db48804f8c0954dab52bf3467d
delete_tagged_brl just ignores non-elimination rules instead of complaining

diff -r cc4c816dafdc -r a318f7f3a65c src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Mar 19 10:23:09 1997 +0100
+++ b/src/Pure/tactic.ML	Wed Mar 19 10:24:39 1997 +0100
@@ -379,7 +379,7 @@
     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"
+	  | []      => (inet,enet)     (*no major premise: ignore*)
     else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
 end;