src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Mon Apr 09 04:51:28 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Apr 09 21:28:24 2007 +0200
@@ -1258,7 +1258,7 @@
 qed
 
 lemma setsum_product:
-  fixes f :: "nat => ('a::semiring_0_cancel)"
+  fixes f :: "'a => ('b::semiring_0_cancel)"
   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)