# HG changeset patch
# User wenzelm
# Date 1142350174 -3600
# Node ID 4463aee061bc080102678cd60c16a3a93632d3c3
# Parent  a49c0f7c96340da215571a350566d1c96297ace0
ObjectLogic.is_elim;

diff -r a49c0f7c9634 -r 4463aee061bc src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Mar 14 16:29:32 2006 +0100
+++ b/src/Provers/classical.ML	Tue Mar 14 16:29:34 2006 +0100
@@ -178,29 +178,13 @@
     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
 *)
 
-local
-
-fun equal_concl concl prop =
-  concl aconv Logic.strip_assums_concl prop;
-
-fun is_elim rule =
-  let
-    val thy = Thm.theory_of_thm rule;
-    val concl = Thm.concl_of rule;
-  in
-    Term.is_Var (ObjectLogic.drop_judgment thy concl) andalso
-    exists (equal_concl concl) (Thm.prems_of rule)
-  end;
-
-in
-
 fun classical_rule rule =
-  if is_elim rule then
+  if ObjectLogic.is_elim rule then
     let
       val rule' = rule RS classical;
       val concl' = Thm.concl_of rule';
       fun redundant_hyp goal =
-         equal_concl concl' goal orelse
+        concl' aconv Logic.strip_assums_concl goal orelse
           (case Logic.strip_assums_hyp goal of
             hyp :: hyps => exists (fn t => t aconv hyp) hyps
           | _ => false);
@@ -215,7 +199,6 @@
     in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end
   else rule;
 
-end;
 
 
 (*** Useful tactics for classical reasoning ***)