diff -r 550a8ecffe0c -r d37babdf5cae src/HOL/Multivariate_Analysis/L2_Norm.thy
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Thu Mar 03 18:43:15 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Thu Mar 03 21:43:06 2011 +0100
@@ -44,7 +44,7 @@
   assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
   shows "setL2 f K \<le> setL2 g K"
   unfolding setL2_def
-  by (simp add: setsum_nonneg setsum_mono power_mono prems)
+  by (simp add: setsum_nonneg setsum_mono power_mono assms)
 
 lemma setL2_strict_mono:
   assumes "finite K" and "K \<noteq> {}"