src/Pure/variable.ML
changeset 21799 a85e3bbc76fb
parent 21683 b90fa6c8e062
child 22568 ed7aa5a350ef
     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