# HG changeset patch
# User wenzelm
# Date 1192547175 -7200
# Node ID 71cd45fdf33212f9a0a26db031329321f8a1e3fb
# Parent  0dc445970b4be7b78aff020a47f9669352ae115e
add_bind: close_schematic_term;

diff -r 0dc445970b4b -r 71cd45fdf332 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Oct 16 17:06:13 2007 +0200
+++ b/src/Pure/variable.ML	Tue Oct 16 17:06:15 2007 +0200
@@ -228,11 +228,9 @@
 fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
   | add_bind ((x, i), SOME t) =
       let
-        val T = Term.fastype_of t;
-        val t' =
-          if null (Term.hidden_polymorphism t T) then t
-          else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
-      in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end;
+        val u = Term.close_schematic_term t;
+        val U = Term.fastype_of u;
+      in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
 
 val add_binds = fold add_bind;