src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy

   then show ?thesis
     unfolding nn_integral_def_finite SUP_def by simp
 qed
 
 lemma nn_integral_count_space_indicator:
-  assumes "NO_MATCH (X::'a set) (UNIV::'a set)"
+  assumes "NO_MATCH (UNIV::'a set) (X::'a set)"
   shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)"
   by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
 
 lemma nn_integral_count_space_eq:
   "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow>