diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -932,7 +932,7 @@
         have "a * u x < 1 * u x"
           by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
         also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)
-        finally obtain i where "a * u x < f i x" unfolding SUP_def
+        finally obtain i where "a * u x < f i x"
           by (auto simp add: less_SUP_iff)
         hence "a * u x \<le> f i x" by auto
         thus ?thesis using \<open>x \<in> space M\<close> by auto
@@ -2042,7 +2042,7 @@
     by (auto intro!: SUP_least SUP_upper nn_integral_mono)
 next
   have "\<And>x. \<exists>g. incseq g \<and> range g \<subseteq> (\<lambda>i. f i x) ` Y \<and> (SUP i:Y. f i x) = (SUP i. g i)"
-    unfolding Sup_class.SUP_def by(rule Sup_countable_SUP[unfolded Sup_class.SUP_def])(simp add: nonempty)
+    by (rule Sup_countable_SUP) (simp add: nonempty)
   then obtain g where incseq: "\<And>x. incseq (g x)"
     and range: "\<And>x. range (g x) \<subseteq> (\<lambda>i. f i x) ` Y"
     and sup: "\<And>x. (SUP i:Y. f i x) = (SUP i. g x i)" by moura
@@ -2088,8 +2088,8 @@
           assume "x \<in> {..<m}"
           hence "x < m" by simp
           have "g x n = f (I x) x" by(simp add: I)
-          also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding SUP_def Sup_fun_def image_image
-            using \<open>x \<in> {..<m}\<close> by(rule Sup_upper[OF imageI])
+          also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding Sup_fun_def image_image
+            using \<open>x \<in> {..<m}\<close> by (rule Sup_upper [OF imageI])
           also have "\<dots> = f (I m') x" unfolding m' by simp
           finally show "g x n \<le> f (I m') x" .
         qed
@@ -2264,7 +2264,7 @@
       by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm)
   qed
   then show ?thesis
-    unfolding nn_integral_def_finite SUP_def by simp
+    unfolding nn_integral_def_finite by (simp cong del: strong_SUP_cong)
 qed
 
 lemma nn_integral_count_space_indicator: