--- a/src/ZF/Constructible/Relative.thy Wed Oct 30 12:18:23 2002 +0100
+++ b/src/ZF/Constructible/Relative.thy Wed Oct 30 12:44:18 2002 +0100
@@ -627,7 +627,7 @@
text{*Probably the premise and conclusion are equivalent*}
lemma (in M_trivial) strong_replacementI [rule_format]:
- "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
+ "[| \<forall>B[M]. separation(M, %u. \<exists>x[M]. x\<in>B & P(x,u)) |]
==> strong_replacement(M,P)"
apply (simp add: strong_replacement_def, clarify)
apply (frule replacementD [OF replacement], assumption, clarify)