now uses equalityCE, which usually is more efficent than equalityE

--- a/src/HOL/Set.ML	Thu Jun 29 12:14:04 2000 +0200
+++ b/src/HOL/Set.ML	Thu Jun 29 12:14:45 2000 +0200
@@ -210,14 +210,14 @@
 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
 qed "equalityE";
 
-AddEs [equalityE];
-
 val major::prems = Goal
     "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
 by (rtac (major RS equalityE) 1);
 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
 qed "equalityCE";
 
+AddEs [equalityCE];
+
 (*Lemma for creating induction formulae -- for "pattern matching" on p
   To make the induction hypotheses usable, apply "spec" or "bspec" to
   put universal quantifiers over the free variables in p. *)