1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -653,7 +653,7 @@
     1.4      measure (density (count_space UNIV) (ereal \<circ> f)) {x} \<noteq> 0"
     1.5      by (simp add: AE_density nonneg measure_def emeasure_density max_def)
     1.6    show "prob_space (density (count_space UNIV) (ereal \<circ> f))"
     1.7 -    by default (simp add: emeasure_density prob)
     1.8 +    by standard (simp add: emeasure_density prob)
     1.9  qed simp
    1.10  
    1.11  lemma pmf_embed_pmf: "pmf embed_pmf x = f x"