1.1 --- a/src/Pure/tactic.ML	Wed Mar 19 10:23:09 1997 +0100
     1.2 +++ b/src/Pure/tactic.ML	Wed Mar 19 10:24:39 1997 +0100
     1.3 @@ -379,7 +379,7 @@
     1.4      if eres then 
     1.5  	case prems_of th of
     1.6  	    prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
     1.7 -	  | [] => error"delete_brl: elimination rule with no premises"
     1.8 +	  | []      => (inet,enet)     (*no major premise: ignore*)
     1.9      else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
    1.10  end;
    1.11