src/HOL/Probability/Probability_Mass_Function.thy

   fix x show "measure (density (count_space UNIV) (ennreal \<circ> f)) {x} = f x"
     by transfer (simp add: measure_def emeasure_density nonneg max_def)
 qed
 
 lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \<noteq> 0}"
-by(auto simp add: set_pmf_eq assms pmf_embed_pmf)
+by(auto simp add: set_pmf_eq pmf_embed_pmf)
 
 end
 
 lemma embed_pmf_transfer:
   "rel_fun (eq_onp (\<lambda>f. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ennreal (f x) \<partial>count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\<lambda>f. density (count_space UNIV) (ennreal \<circ> f)) embed_pmf"

   by (subst nn_integral_indicator[symmetric], simp)
      (simp add: S_finite S_not_empty card_gt_0_iff indicator_def setsum.If_cases divide_ennreal
                 ennreal_of_nat_eq_real_of_nat nn_integral_pmf_of_set)
 
 lemma measure_pmf_of_set: "measure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
-  using emeasure_pmf_of_set[OF assms, of A]
+  using emeasure_pmf_of_set[of A]
   by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure)
 
 end
 
 lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"