diff -r de51a86fc903 -r cc97b347b301 src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/IMP/ACom.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -104,7 +104,7 @@
 apply(induction c arbitrary: f p)
 apply (auto simp: anno_def nth_append nth_Cons numeral_eq_Suc shift_def
             split: nat.split)
-  apply (metis add_Suc_right add_diff_inverse nat_add_commute)
+  apply (metis add_Suc_right add_diff_inverse add.commute)
  apply(rule_tac f=f in arg_cong)
  apply arith
 apply (metis less_Suc_eq)