diff -r 33147ecac5f9 -r a1ba833d6b61 src/ZF/Integ/EquivClass.thy
--- 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