src/Pure/variable.ML
changeset 25051 71cd45fdf332
parent 24848 5dbbd33c3236
child 25316 17c183417f93
     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