diff -r fe5b796d6b2a -r b6bda9140e39 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Mar 23 15:08:02 2015 +0100
@@ -1955,7 +1955,7 @@
 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)