diff -r 35807a5d8dc2 -r 2a1953f0d20d src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Mar 25 20:15:39 2012 +0200
@@ -281,7 +281,7 @@
 lemma scaleR_2:
   fixes x :: "'a::real_vector"
   shows "scaleR 2 x = x + x"
-unfolding one_add_one_is_two [symmetric] scaleR_left_distrib by simp
+unfolding one_add_one [symmetric] scaleR_left_distrib by simp
 
 lemma vector_choose_size: "0 <= c ==> \<exists>(x::'a::euclidean_space). norm x = c"
   apply (rule exI[where x="c *\<^sub>R basis 0 ::'a"]) using DIM_positive[where 'a='a] by auto