diff -r 21010d2b41e7 -r 58a0757031dd src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Thu May 20 23:22:37 2010 +0200
+++ b/src/HOL/Probability/Borel.thy	Thu May 20 21:19:38 2010 -0700
@@ -397,8 +397,7 @@
   { fix w
     from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
       by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
-                linorder_not_le order_refl order_trans less_le
-                xt1(7) zero_less_divide_1_iff) }
+                less_le_trans zero_less_divide_1_iff) }
   hence "{w \<in> space M. a \<le> inverse (f w)} =
     {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
   with Int assms[unfolded borel_measurable_gr_iff]