merged

--- a/src/HOL/Int.thy	Wed Jul 29 12:13:21 2009 +0200
+++ b/src/HOL/Int.thy	Wed Jul 29 16:43:02 2009 +0200
@@ -1000,11 +1000,11 @@
   Converting numerals 0 and 1 to their abstract versions.
 *}
 
-lemma numeral_0_eq_0 [simp]:
+lemma numeral_0_eq_0 [simp, code_post]:
   "Numeral0 = (0::'a::number_ring)"
   unfolding number_of_eq numeral_simps by simp
 
-lemma numeral_1_eq_1 [simp]:
+lemma numeral_1_eq_1 [simp, code_post]:
   "Numeral1 = (1::'a::number_ring)"
   unfolding number_of_eq numeral_simps by simp
 

--- a/src/Tools/Code/code_thingol.ML	Wed Jul 29 12:13:21 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Jul 29 16:43:02 2009 +0200
@@ -579,15 +579,15 @@
       translate_app thy algbr funcgr thm ((c, ty), [])
   | translate_term thy algbr funcgr thm (Free (v, _)) =
       pair (IVar (SOME v))
-  | translate_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
+  | translate_term thy algbr funcgr thm (Abs (v, ty, t)) =
       let
-        val (v, t) = Syntax.variant_abs abs;
-        val v' = if member (op =) (Term.add_free_names t []) v
-          then SOME v else NONE
+        val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
+        val v'' = if member (op =) (Term.add_free_names t' []) v'
+          then SOME v' else NONE
       in
         translate_typ thy algbr funcgr ty
-        ##>> translate_term thy algbr funcgr thm t
-        #>> (fn (ty, t) => (v', ty) `|=> t)
+        ##>> translate_term thy algbr funcgr thm t'
+        #>> (fn (ty, t) => (v'', ty) `|=> t)
       end
   | translate_term thy algbr funcgr thm (t as _ $ _) =
       case strip_comb t