# HG changeset patch
# User wenzelm
# Date 1165952966 -3600
# Node ID a85e3bbc76fb368fa08609e104e9bec5937bff7c
# Parent  a1399df6ecf332cf7edbb4dc61f3076a982a0187
tuned expand_binds;

diff -r a1399df6ecf3 -r a85e3bbc76fb src/Pure/variable.ML
--- 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;