diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -2507,7 +2507,7 @@
     fix i assume i:"i<DIM('a)" thus "0 < x $$ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
       unfolding dist_norm  by(auto simp add: inner_simps euclidean_component_def dot_basis elim!:allE[where x=i])
   next have **:"dist x (x + (e / 2) *\<^sub>R basis 0) < e" using  `e>0`
-      unfolding dist_norm by(auto intro!: mult_strict_left_mono_comm)
+      unfolding dist_norm by(auto intro!: mult_strict_left_mono)
     have "\<And>i. i<DIM('a) \<Longrightarrow> (x + (e / 2) *\<^sub>R basis 0) $$ i = x$$i + (if i = 0 then e/2 else 0)"
       unfolding euclidean_component_def by(auto simp add:inner_simps dot_basis)
     hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)} = setsum (\<lambda>i. x$$i + (if 0 = i then e/2 else 0)) {..<DIM('a)}"