changeset 21799 | a85e3bbc76fb |
parent 21683 | b90fa6c8e062 |
child 22568 | ed7aa5a350ef |
--- a/src/Pure/variable.ML Tue Dec 12 20:49:25 2006 +0100 +++ b/src/Pure/variable.ML Tue Dec 12 20:49:26 2006 +0100 @@ -236,12 +236,8 @@ fun expand_binds ctxt = let val binds = binds_of ctxt; - fun expand (t as Var (xi, T)) = - (case Vartab.lookup binds xi of - SOME u => Envir.expand_atom T u - | NONE => t) - | expand t = t; - in Envir.beta_norm o Term.map_aterms expand end; + val get = fn Var (xi, _) => Vartab.lookup binds xi | _ => NONE; + in Envir.beta_norm o Envir.expand_term get end;