add_bind: close_schematic_term;
authorwenzelm
Tue Oct 16 17:06:15 2007 +0200 (2007-10-16)
changeset 2505171cd45fdf332
parent 25050 0dc445970b4b
child 25052 a014d544f54d
add_bind: close_schematic_term;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Tue Oct 16 17:06:13 2007 +0200
     1.2 +++ b/src/Pure/variable.ML	Tue Oct 16 17:06:15 2007 +0200
     1.3 @@ -228,11 +228,9 @@
     1.4  fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
     1.5    | add_bind ((x, i), SOME t) =
     1.6        let
     1.7 -        val T = Term.fastype_of t;
     1.8 -        val t' =
     1.9 -          if null (Term.hidden_polymorphism t T) then t
    1.10 -          else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
    1.11 -      in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end;
    1.12 +        val u = Term.close_schematic_term t;
    1.13 +        val U = Term.fastype_of u;
    1.14 +      in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
    1.15  
    1.16  val add_binds = fold add_bind;
    1.17