--- a/src/ZF/Integ/EquivClass.thy Wed Jul 09 12:41:47 2003 +0200
+++ b/src/ZF/Integ/EquivClass.thy Thu Jul 10 17:14:41 2003 +0200
@@ -125,9 +125,9 @@
(*Conversion rule*)
lemma UN_equiv_class:
"[| equiv(A,r); congruent(r,b); a: A |] ==> (UN x:r``{a}. b(x)) = b(a)"
-apply (rule trans [OF refl [THEN UN_cong] UN_constant])
-apply (erule_tac [2] equiv_class_self)
-prefer 2 apply assumption
+apply (subgoal_tac "\<forall>x \<in> r``{a}. b(x) = b(a)")
+ apply simp
+ apply (blast intro: equiv_class_self)
apply (unfold equiv_def sym_def congruent_def, blast)
done