diff -r d5ff8b782b29 -r fee7cfa69c50 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -33,7 +33,7 @@
 
 lemma foldSetD_closed:
   "[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D 
-      |] ==> z \<in> D";
+      |] ==> z \<in> D"
   by (erule foldSetD.cases) auto
 
 lemma Diff1_foldSetD:
@@ -72,7 +72,7 @@
   and f_closed [simp, intro!]: "!!x y. [| x \<in> B; y \<in> D |] ==> f x y \<in> D"
 
 lemma (in LCD) foldSetD_closed [dest]:
-  "(A, z) \<in> foldSetD D f e ==> z \<in> D";
+  "(A, z) \<in> foldSetD D f e ==> z \<in> D"
   by (erule foldSetD.cases) auto
 
 lemma (in LCD) Diff1_foldSetD: