diff -r 1266f04f42ec -r 1b2bae06c796 src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Mon Feb 08 17:12:24 2010 +0100
+++ b/src/HOL/Tools/nat_arith.ML	Mon Feb 08 17:12:27 2010 +0100
@@ -50,8 +50,8 @@
   val mk_sum = mk_norm_sum;
   val dest_sum = dest_sum;
   val prove_conv = Arith_Data.prove_conv2;
-  val norm_tac1 = Arith_Data.simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
-    @{thm "add_0"}, @{thm "add_0_right"}];
+  val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
+    @{thm add_0}, @{thm Nat.add_0_right}];
   val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
   fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
   fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}