src/ZF/AC.thy

--- a/src/ZF/AC.thy	Tue May 14 12:33:42 2002 +0200
+++ b/src/ZF/AC.thy	Wed May 15 10:42:32 2002 +0200
@@ -15,7 +15,7 @@
 (*The same as AC, but no premise a \<in> A*)
 lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
 apply (case_tac "A=0")
-apply (simp add: Pi_empty1, blast)
+apply (simp add: Pi_empty1)
 (*The non-trivial case*)
 apply (blast intro: AC)
 done