diff -r ea49c12f677f -r 05d78159812d src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Thu Mar 27 10:06:36 1997 +0100
+++ b/src/FOL/cladata.ML	Thu Mar 27 10:07:11 1997 +0100
@@ -10,6 +10,7 @@
 (** Applying HypsubstFun to generate hyp_subst_tac **)
 section "Classical Reasoner";
 
+
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data = 
   struct
@@ -23,6 +24,18 @@
 structure Cla = ClassicalFun(Classical_Data);
 open Cla;
 
+(*Better for fast_tac: needs no quantifier duplication!*)
+qed_goal "alt_ex1E" IFOL.thy
+    "[| EX! x.P(x);                                              \
+\       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
+\    |] ==> R"
+ (fn major::prems =>
+  [ (rtac (major RS ex1E) 1),
+    (REPEAT (ares_tac (allI::prems) 1)),
+    (etac (dup_elim allE) 1),
+    (IntPr.fast_tac 1)]);
+
+
 (*Propositional rules 
   -- iffCE might seem better, but in the examples in ex/cla
      run about 7% slower than with iffE*)
@@ -30,8 +43,8 @@
                        addSEs [conjE,disjE,impCE,FalseE,iffE];
 
 (*Quantifier rules*)
-val FOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 
-                     addSEs [exE,ex1E] addEs [allE];
+val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
+                     addSEs [exE,alt_ex1E] addEs [allE];
 
 
 exception CS_DATA of claset;