diff -r 220bc60c2387 -r 72a02e3dec7e src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Jan 15 18:49:42 2011 +0100
+++ b/src/Provers/classical.ML	Sat Jan 15 20:51:22 2011 +0100
@@ -153,7 +153,7 @@
 *)
 
 fun classical_rule rule =
-  if Object_Logic.is_elim rule then
+  if is_some (Object_Logic.elim_concl rule) then
     let
       val rule' = rule RS classical;
       val concl' = Thm.concl_of rule';