diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Nat.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -1356,7 +1356,7 @@
 end
 
 lemma of_nat_id [simp]: "of_nat n = n"
-  by (induct n) (auto simp add: One_nat_def)
+  by (induct n) simp_all
 
 lemma of_nat_eq_id [simp]: "of_nat = id"
   by (auto simp add: expand_fun_eq)
@@ -1619,7 +1619,7 @@
 
 lemma dvd_antisym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   unfolding dvd_def
-  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
+  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc)
 
 text {* @{term "op dvd"} is a partial order *}