src/ZF/Constructible/Relative.thy

--- a/src/ZF/Constructible/Relative.thy	Wed Jun 26 18:38:03 2013 +0200
+++ b/src/ZF/Constructible/Relative.thy	Wed Jun 26 21:48:23 2013 +0200
@@ -753,8 +753,6 @@
      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
       ==> M(RepFun(A,f))"
 apply (simp add: RepFun_def)
-apply (rule strong_replacement_closed)
-apply (auto dest: transM  simp add: univalent_def)
 done
 
 lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"