src/ZF/AC/WO2_AC16.thy

--- a/src/ZF/AC/WO2_AC16.thy	Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/AC/WO2_AC16.thy	Mon Mar 23 21:05:17 2015 +0100
@@ -563,7 +563,7 @@
 apply (elim exE)
 apply (rename_tac h)
 apply (rule_tac x = "\<Union>j<a. recfunAC16 (h,f,j,a) " in exI)
-apply (rule_tac P="%z. ?Y & (\<forall>x \<in> z. ?Z (x))" 
+apply (rule_tac P="%z. Y & (\<forall>x \<in> z. Z(x))"  for Y Z
        in bij_is_surj [THEN surj_image_eq, THEN subst], assumption)
 apply (rule lemma_simp_induct)
 apply (blast del: conjI notI