--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 23 11:17:13 2010 +0200
@@ -5678,7 +5678,7 @@
next
case (Suc m)
hence "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"
- using `0 \<le> c` using mult_mono1_class.mult_mono1[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
+ using `0 \<le> c` using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
thus ?case using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
unfolding fzn and mult_le_cancel_left by auto
qed