
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -132,7 +132,7 @@
       by (auto intro!: exI[of _ "from_nat i"])
   qed
   have **: "range ?A' = range A"
-    using surj_range[OF surj_from_nat]
+    using surj_from_nat
     by (auto simp: image_compose intro!: imageI)
   show ?thesis unfolding * ** ..
 qed




