--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 26 20:52:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 26 21:09:36 2010 +0100
@@ -19,7 +19,7 @@
lemma injective_scaleR:
assumes "(c :: real) ~= 0"
shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
-by (metis assms datatype_injI injI real_vector.scale_cancel_left)
+ by (metis assms injI real_vector.scale_cancel_left)
lemma linear_add_cmul:
fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"