diff -r 5c579bb9adb1 -r 98cf1c823c48 src/HOL/Random.thy
--- a/src/HOL/Random.thy	Sun Jun 03 19:06:56 2018 +0200
+++ b/src/HOL/Random.thy	Wed Jun 06 11:12:37 2018 +0200
@@ -116,7 +116,7 @@
 lemma select_weight_drop_zero:
   "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
 proof -
-  have "sum_list (map fst (filter (\<lambda>(k, _). 0 < k) xs)) = sum_list (map fst xs)"
+  have "sum_list (map fst [(k, _)\<leftarrow>xs . 0 < k]) = sum_list (map fst xs)"
     by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
   then show ?thesis by (simp only: select_weight_def pick_drop_zero)
 qed