tuned expand_binds;
authorwenzelm
Tue Dec 12 20:49:26 2006 +0100 (2006-12-12)
changeset 21799a85e3bbc76fb
parent 21798 a1399df6ecf3
child 21800 6035bfcd72d8
tuned expand_binds;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Tue Dec 12 20:49:25 2006 +0100
     1.2 +++ b/src/Pure/variable.ML	Tue Dec 12 20:49:26 2006 +0100
     1.3 @@ -236,12 +236,8 @@
     1.4  fun expand_binds ctxt =
     1.5    let
     1.6      val binds = binds_of ctxt;
     1.7 -    fun expand (t as Var (xi, T)) =
     1.8 -          (case Vartab.lookup binds xi of
     1.9 -            SOME u => Envir.expand_atom T u
    1.10 -          | NONE => t)
    1.11 -      | expand t = t;
    1.12 -  in Envir.beta_norm o Term.map_aterms expand end;
    1.13 +    val get = fn Var (xi, _) => Vartab.lookup binds xi | _ => NONE;
    1.14 +  in Envir.beta_norm o Envir.expand_term get end;
    1.15  
    1.16  
    1.17