src/Provers/make_elim.ML

--- a/src/Provers/make_elim.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Provers/make_elim.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -41,7 +41,7 @@
 	      | rl'::_ => making (i+1,rl')
     in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl')))  end
     handle (*in default, use the previous version, which never fails*)
-	   THM _ => Tactic.make_elim rl | LIST _ => Tactic.make_elim rl;
+	   THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl;
 
 end