diff -r e58623a33ba5 -r cdc6d8cbf770 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Tue Dec 17 20:21:22 2013 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy	Tue Dec 17 22:34:26 2013 +0100
@@ -78,7 +78,7 @@
 
 lemma [code]:
   "Divides.divmod_nat m n = (m div n, m mod n)"
-  by (simp add: prod_eq_iff)
+  by (fact divmod_nat_div_mod)
 
 lemma [code]:
   "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
@@ -96,7 +96,7 @@
   "num_of_nat = num_of_integer \<circ> of_nat"
   by transfer (simp add: fun_eq_iff)
 
-lemma (in semiring_1) of_nat_code:
+lemma (in semiring_1) of_nat_code_if:
   "of_nat n = (if n = 0 then 0
      else let
        (m, q) = divmod_nat n 2;
@@ -105,12 +105,11 @@
 proof -
   from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
   show ?thesis
-    by (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
-      of_nat_add [symmetric])
+    by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
       (simp add: * mult_commute of_nat_mult add_commute)
 qed
 
-declare of_nat_code [code]
+declare of_nat_code_if [code]
 
 definition int_of_nat :: "nat \<Rightarrow> int" where
   [code_abbrev]: "int_of_nat = of_nat"
@@ -134,13 +133,13 @@
            [typerep.Typerep (STR ''Code_Numeral.integer'') [],
          typerep.Typerep (STR ''Nat.nat'') []]))
      (term_of_class.term_of (integer_of_nat n))"
-by(simp add: term_of_anything)
+  by (simp add: term_of_anything)
 
 lemma nat_of_integer_code_post [code_post]:
   "nat_of_integer 0 = 0"
   "nat_of_integer 1 = 1"
   "nat_of_integer (numeral k) = numeral k"
-by(transfer, simp)+
+  by (transfer, simp)+
 
 code_identifier
   code_module Code_Target_Nat \<rightharpoonup>