src/ZF/OrdQuant.thy

--- a/src/ZF/OrdQuant.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/OrdQuant.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -273,7 +273,7 @@
 lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
 by blast
 
-lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))";
+lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))"
 by (simp add: rall_def atomize_all atomize_imp)
 
 declare atomize_rall [symmetric, rulify]