src/Provers/classical.ML
changeset 41581 72a02e3dec7e
parent 36960 01594f816e3a
child 42361 23f352990944
     1.1 --- a/src/Provers/classical.ML	Sat Jan 15 18:49:42 2011 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Jan 15 20:51:22 2011 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4  *)
     1.5  
     1.6  fun classical_rule rule =
     1.7 -  if Object_Logic.is_elim rule then
     1.8 +  if is_some (Object_Logic.elim_concl rule) then
     1.9      let
    1.10        val rule' = rule RS classical;
    1.11        val concl' = Thm.concl_of rule';