diff -r 7f6838b3474a -r 5b1e1432c320 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 06 07:45:18 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 06 07:48:59 2011 -0700
@@ -420,7 +420,7 @@
   assumes x: "0 \<le> x" and y: "0 \<le> y"
   shows "sqrt (x + y) \<le> sqrt x + sqrt y"
 apply (rule power2_le_imp_le)
-apply (simp add: real_sum_squared_expand x y)
+apply (simp add: power2_sum x y)
 apply (simp add: mult_nonneg_nonneg x y)
 apply (simp add: x y)
 done