--- a/src/HOL/Probability/Euclidean_Lebesgue.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Probability/Euclidean_Lebesgue.thy Mon Sep 13 11:13:15 2010 +0200
@@ -104,7 +104,7 @@
from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
show ?ilim using mono lim i by auto
have "(SUP i. f i) = u" using mono lim SUP_Lim_pinfreal
- unfolding ext_iff SUPR_fun_expand mono_def by auto
+ unfolding fun_eq_iff SUPR_fun_expand mono_def by auto
moreover have "(SUP i. f i) \<in> borel_measurable M"
using i by (rule borel_measurable_SUP)
ultimately show "u \<in> borel_measurable M" by simp