abstractions: desymbolize name hint
authorhaftmann
Wed Jul 29 16:42:47 2009 +0200 (2009-07-29)
changeset 322733c395fc7ec5e
parent 32272 cc1bf9077167
child 32274 e7f275d203bc
abstractions: desymbolize name hint
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jul 29 16:42:47 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jul 29 16:42:47 2009 +0200
     1.3 @@ -579,15 +579,15 @@
     1.4        translate_app thy algbr funcgr thm ((c, ty), [])
     1.5    | translate_term thy algbr funcgr thm (Free (v, _)) =
     1.6        pair (IVar (SOME v))
     1.7 -  | translate_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
     1.8 +  | translate_term thy algbr funcgr thm (Abs (v, ty, t)) =
     1.9        let
    1.10 -        val (v, t) = Syntax.variant_abs abs;
    1.11 -        val v' = if member (op =) (Term.add_free_names t []) v
    1.12 -          then SOME v else NONE
    1.13 +        val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
    1.14 +        val v'' = if member (op =) (Term.add_free_names t' []) v'
    1.15 +          then SOME v' else NONE
    1.16        in
    1.17          translate_typ thy algbr funcgr ty
    1.18 -        ##>> translate_term thy algbr funcgr thm t
    1.19 -        #>> (fn (ty, t) => (v', ty) `|=> t)
    1.20 +        ##>> translate_term thy algbr funcgr thm t'
    1.21 +        #>> (fn (ty, t) => (v'', ty) `|=> t)
    1.22        end
    1.23    | translate_term thy algbr funcgr thm (t as _ $ _) =
    1.24        case strip_comb t