tuned expand_binds;

--- 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;