diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Oct 13 09:21:15 2015 +0200
@@ -163,7 +163,7 @@
show ?thesis
by (intro measurable_compose_countable'[where f="\a b. f (fst b, a)" and g=snd and I=A,
- unfolded pair_collapse] assms)
+ unfolded prod.collapse] assms)
measurable
qed
@@ -177,7 +177,7 @@
show ?thesis
by (intro measurable_compose_countable'[where f="\a b. f (a, snd b)" and g=fst and I=A,
- unfolded pair_collapse] assms)
+ unfolded prod.collapse] assms)
measurable
qed