1.1 --- a/src/HOL/Library/Code_Integer.thy	Mon Mar 26 19:03:27 2012 +0200
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Mon Mar 26 19:04:17 2012 +0200
     1.3 @@ -16,11 +16,13 @@
     1.4    "nat k = (if k \<le> 0 then 0 else
     1.5       let
     1.6         (l, j) = divmod_int k 2;
     1.7 -       l' = 2 * nat l
     1.8 +       n = nat l;
     1.9 +       l' = n + n
    1.10       in if j = 0 then l' else Suc l')"
    1.11  proof -
    1.12    have "2 = nat 2" by simp
    1.13    show ?thesis
    1.14 +    apply (subst nat_mult_2 [symmetric])
    1.15      apply (auto simp add: Let_def divmod_int_mod_div not_le
    1.16       nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int)
    1.17      apply (unfold `2 = nat 2`)