--- a/src/HOL/Probability/Independent_Family.thy Sun Oct 16 22:43:51 2016 +0200
+++ b/src/HOL/Probability/Independent_Family.thy Mon Oct 17 11:46:22 2016 +0200
@@ -991,7 +991,7 @@
unfolding indep_var_def .
qed
-lemma (in prob_space) indep_vars_setsum:
+lemma (in prob_space) indep_vars_sum:
fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
shows "indep_var borel (X i) borel (\<lambda>\<omega>. \<Sum>i\<in>I. X i \<omega>)"