diff -r ef1e0cb80fde -r 949d93804740 src/HOL/Random.thy
--- a/src/HOL/Random.thy	Tue May 22 14:12:15 2018 +0200
+++ b/src/HOL/Random.thy	Tue May 22 11:08: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 [(k, _)\<leftarrow>xs . 0 < k]) = sum_list (map fst xs)"
+  have "sum_list (map fst (filter (\<lambda>(k, _). 0 < k) xs)) = 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