diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Probability/PMF_Impl.thy
--- a/src/HOL/Probability/PMF_Impl.thy	Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Probability/PMF_Impl.thy	Fri Jul 22 08:02:37 2016 +0200
@@ -402,9 +402,9 @@
                (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
 proof -
   from assms have wf: "pmf_of_list_wf xs" by (intro pmf_of_list_wfI) force
-  moreover from this assms have "set_pmf (pmf_of_list xs) = fst ` set xs"
+  with assms have "set_pmf (pmf_of_list xs) = fst ` set xs"
     by (intro set_pmf_of_list_eq) auto
-  ultimately show ?thesis
+  with wf show ?thesis
     by (intro mapping_of_pmfI) (auto simp: lookup_tabulate pmf_pmf_of_list)
 qed