src/HOL/Probability/Probability_Mass_Function.thy

       using Cons(1) by (intro Cons) simp_all
     finally show ?case by (simp add: case_prod_unfold)
   qed simp
   also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. ennreal p * (\<integral>\<^sup>+ x. indicator {x'} x \<partial>count_space UNIV))"
     using assms(1)
-    by (intro sum_list_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric])
+    by (simp cong: map_cong only: case_prod_unfold, subst nn_integral_cmult [symmetric])
        (auto intro!: assms(1) simp: max_def times_ereal.simps [symmetric] mult_ac ereal_indicator
              simp del: times_ereal.simps)+
   also from assms have "\<dots> = sum_list (map snd xs)" by (simp add: case_prod_unfold sum_list_ennreal)
   also have "\<dots> = 1" using assms(2) by simp
   finally show ?thesis .