1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4  
     1.5    show ?thesis
     1.6      by (intro measurable_compose_countable'[where f="\<lambda>a b. f (fst b, a)" and g=snd and I=A,
     1.7 -                                            unfolded pair_collapse] assms)
     1.8 +                                            unfolded prod.collapse] assms)
     1.9          measurable
    1.10  qed
    1.11  
    1.12 @@ -177,7 +177,7 @@
    1.13  
    1.14    show ?thesis
    1.15      by (intro measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A,
    1.16 -                                            unfolded pair_collapse] assms)
    1.17 +                                            unfolded prod.collapse] assms)
    1.18          measurable
    1.19  qed
    1.20