merged
authorhaftmann
Wed Jul 29 16:43:02 2009 +0200 (2009-07-29)
changeset 32274e7f275d203bc
parent 32271 378ebd64447d
parent 32273 3c395fc7ec5e
child 32275 b10cbf4d3f55
child 32287 65d5c5b30747
merged
     1.1 --- a/src/HOL/Int.thy	Wed Jul 29 12:13:21 2009 +0200
     1.2 +++ b/src/HOL/Int.thy	Wed Jul 29 16:43:02 2009 +0200
     1.3 @@ -1000,11 +1000,11 @@
     1.4    Converting numerals 0 and 1 to their abstract versions.
     1.5  *}
     1.6  
     1.7 -lemma numeral_0_eq_0 [simp]:
     1.8 +lemma numeral_0_eq_0 [simp, code_post]:
     1.9    "Numeral0 = (0::'a::number_ring)"
    1.10    unfolding number_of_eq numeral_simps by simp
    1.11  
    1.12 -lemma numeral_1_eq_1 [simp]:
    1.13 +lemma numeral_1_eq_1 [simp, code_post]:
    1.14    "Numeral1 = (1::'a::number_ring)"
    1.15    unfolding number_of_eq numeral_simps by simp
    1.16  
     2.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jul 29 12:13:21 2009 +0200
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jul 29 16:43:02 2009 +0200
     2.3 @@ -579,15 +579,15 @@
     2.4        translate_app thy algbr funcgr thm ((c, ty), [])
     2.5    | translate_term thy algbr funcgr thm (Free (v, _)) =
     2.6        pair (IVar (SOME v))
     2.7 -  | translate_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
     2.8 +  | translate_term thy algbr funcgr thm (Abs (v, ty, t)) =
     2.9        let
    2.10 -        val (v, t) = Syntax.variant_abs abs;
    2.11 -        val v' = if member (op =) (Term.add_free_names t []) v
    2.12 -          then SOME v else NONE
    2.13 +        val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
    2.14 +        val v'' = if member (op =) (Term.add_free_names t' []) v'
    2.15 +          then SOME v' else NONE
    2.16        in
    2.17          translate_typ thy algbr funcgr ty
    2.18 -        ##>> translate_term thy algbr funcgr thm t
    2.19 -        #>> (fn (ty, t) => (v', ty) `|=> t)
    2.20 +        ##>> translate_term thy algbr funcgr thm t'
    2.21 +        #>> (fn (ty, t) => (v'', ty) `|=> t)
    2.22        end
    2.23    | translate_term thy algbr funcgr thm (t as _ $ _) =
    2.24        case strip_comb t