diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Probability/Borel.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -1031,7 +1031,7 @@
   have "f -` {\<omega>} \<inter> space M = {x\<in>space M. f x = \<omega>}" by auto
   with * have **: "{x\<in>space M. f x = \<omega>} \<in> sets M" by simp
   have f: "f = (\<lambda>x. if f x = \<omega> then \<omega> else Real (real (f x)))"
-    by (simp add: expand_fun_eq Real_real)
+    by (simp add: ext_iff Real_real)
   show "f \<in> borel_measurable M"
     apply (subst f)
     apply (rule measurable_If)
@@ -1264,7 +1264,7 @@
 proof -
   have *: "(\<lambda>x. f x + g x) =
      (\<lambda>x. if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else Real (real (f x) + real (g x)))"
-     by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex)
+     by (auto simp: ext_iff pinfreal_noteq_omega_Ex)
   show ?thesis using assms unfolding *
     by (auto intro!: measurable_If)
 qed
@@ -1276,7 +1276,7 @@
   have *: "(\<lambda>x. f x * g x) =
      (\<lambda>x. if f x = 0 then 0 else if g x = 0 then 0 else if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else
       Real (real (f x) * real (g x)))"
-     by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex)
+     by (auto simp: ext_iff pinfreal_noteq_omega_Ex)
   show ?thesis using assms unfolding *
     by (auto intro!: measurable_If)
 qed