diff -r 4d0878d54ca5 -r 501b9bbd0d6e src/HOL/NSA/HSeries.thy
--- a/src/HOL/NSA/HSeries.thy	Fri Mar 30 10:41:27 2012 +0200
+++ b/src/HOL/NSA/HSeries.thy	Fri Mar 30 11:16:35 2012 +0200
@@ -114,7 +114,7 @@
 lemma sumhr_minus_one_realpow_zero [simp]: 
      "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
 unfolding sumhr_app
-by transfer (simp del: power_Suc add: nat_mult_2 [symmetric])
+by transfer (simp del: power_Suc add: mult_2 [symmetric])
 
 lemma sumhr_interval_const:
      "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na