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="\<lambda>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="\<lambda>a b. f (a, snd b)" and g=fst and I=A,
-                                            unfolded pair_collapse] assms)
+                                            unfolded prod.collapse] assms)
         measurable
 qed