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;