diff -r 34023a586608 -r aefb4a8da31f src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Limits.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -1239,7 +1239,7 @@
 proof (induct n)
   case (Suc n)
   have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)"
-    by (simp add: field_simps real_of_nat_Suc mult_nonneg_nonneg x)
+    by (simp add: field_simps real_of_nat_Suc x)
   also have "\<dots> \<le> (x + 1)^Suc n"
     using Suc x by (simp add: mult_left_mono)
   finally show ?case .