diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Presburger.thy	Tue Sep 06 19:03:41 2011 -0700
@@ -308,7 +308,7 @@
   {fix x
     have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
     also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
-      by (simp add:int_distrib zadd_ac)
+      by (simp add:int_distrib add_ac)
     ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast}
   thus ?case ..
 qed