--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri Jul 22 11:00:43 2016 +0200
@@ -1734,7 +1734,7 @@
proof (rule measure_eqI)
fix X assume "X \<in> sets M"
then have X: "X \<subseteq> A" by auto
- moreover with A have "countable X" by (auto dest: countable_subset)
+ moreover from A X have "countable X" by (auto dest: countable_subset)
ultimately have
"emeasure M X = (\<integral>\<^sup>+a. emeasure M {a} \<partial>count_space X)"
"emeasure N X = (\<integral>\<^sup>+a. emeasure N {a} \<partial>count_space X)"