diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -1106,7 +1106,7 @@
     by (rule positive_integral_isoton)
        (auto intro!: borel_measurable_pinfreal_setsum assms positive_integral_mono
                      arg_cong[where f=Sup]
-             simp: isoton_def le_fun_def psuminf_def expand_fun_eq SUPR_def Sup_fun_def)
+             simp: isoton_def le_fun_def psuminf_def ext_iff SUPR_def Sup_fun_def)
   thus ?thesis
     by (auto simp: isoton_def psuminf_def positive_integral_setsum[OF assms])
 qed
@@ -1365,7 +1365,7 @@
     then have *: "(\<lambda>x. g x * indicator A x) = g"
       "\<And>x. g x * indicator A x = g x"
       "\<And>x. g x \<le> f x"
-      by (auto simp: le_fun_def expand_fun_eq indicator_def split: split_if_asm)
+      by (auto simp: le_fun_def ext_iff indicator_def split: split_if_asm)
     from g show "\<exists>x. simple_function (\<lambda>xa. x xa * indicator A xa) \<and> x \<le> f \<and> (\<forall>xa\<in>A. \<omega> \<noteq> x xa) \<and>
       simple_integral g = simple_integral (\<lambda>xa. x xa * indicator A xa)"
       using `A \<in> sets M`[THEN sets_into_space]