diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Fri Jun 27 22:08:55 2014 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Sat Jun 28 09:16:42 2014 +0200
@@ -450,7 +450,7 @@
     by (induct s rule: finite_induct) auto
 next
   case False then show ?thesis using assms
-    by (metis Reals_0 setsum_infinite)
+    by (metis Reals_0 setsum.infinite)
 qed
 
 lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
@@ -459,7 +459,7 @@
     by (induct s rule: finite_induct) auto
 next
   case False then show ?thesis using assms
-    by (metis Reals_1 setprod_infinite)
+    by (metis Reals_1 setprod.infinite)
 qed
 
 lemma Reals_induct [case_names of_real, induct set: Reals]: