diff -r 34618f031ba9 -r cdddd073bff8 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Feb 24 15:45:55 2014 +0000
+++ b/src/HOL/Set_Interval.thy	Mon Feb 24 16:56:04 2014 +0000
@@ -1667,7 +1667,13 @@
 
 lemma setprod_power_distrib:
   fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
-  shows "finite A \<Longrightarrow> setprod f A ^ n = setprod (\<lambda>x. (f x)^n) A"
-  by (induct set: finite) (auto simp: power_mult_distrib)
+  shows "setprod f A ^ n = setprod (\<lambda>x. (f x)^n) A"
+proof (cases "finite A") 
+  case True then show ?thesis 
+    by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
+next
+  case False then show ?thesis 
+    by (metis setprod_infinite power_one)
+qed
 
 end