merged

--- a/src/HOL/Library/Code_Integer.thy	Mon Mar 26 19:18:03 2012 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Mon Mar 26 20:07:41 2012 +0200
@@ -16,11 +16,13 @@
   "nat k = (if k \<le> 0 then 0 else
      let
        (l, j) = divmod_int k 2;
-       l' = 2 * nat l
+       n = nat l;
+       l' = n + n
      in if j = 0 then l' else Suc l')"
 proof -
   have "2 = nat 2" by simp
   show ?thesis
+    apply (subst nat_mult_2 [symmetric])
     apply (auto simp add: Let_def divmod_int_mod_div not_le
      nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int)
     apply (unfold `2 = nat 2`)

--- a/src/HOL/Num.thy	Mon Mar 26 19:18:03 2012 +0200
+++ b/src/HOL/Num.thy	Mon Mar 26 20:07:41 2012 +0200
@@ -1010,12 +1010,12 @@
 subsection {* code module namespace *}
 
 code_modulename SML
-  Numeral Arith
+  Num Arith
 
 code_modulename OCaml
-  Numeral Arith
+  Num Arith
 
 code_modulename Haskell
-  Numeral Arith
+  Num Arith
 
 end

--- a/src/HOL/Proofs/Lambda/Eta.thy	Mon Mar 26 19:18:03 2012 +0200
+++ b/src/HOL/Proofs/Lambda/Eta.thy	Mon Mar 26 20:07:41 2012 +0200
@@ -159,7 +159,7 @@
      apply (slowsimp intro: rtrancl_eta_subst eta_subst)
     apply (blast intro: rtrancl_eta_AppL)
    apply (blast intro: rtrancl_eta_AppR)
-  apply simp;
+  apply simp
   apply (slowsimp intro: rtrancl_eta_Abs free_beta
     iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
   done