changeset 8637 | e86e49aa1631 |
parent 8616 | 90d2fed59be1 |
child 8807 | 0046be1769f9 |
--- a/src/Pure/Isar/proof_context.ML Fri Mar 31 21:56:13 2000 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Mar 31 21:56:23 2000 +0200 @@ -688,7 +688,7 @@ val T = Term.fastype_of t; val t' = if null (Term.term_tvars t \\ Term.typ_tvars T) then t - else Var ((x ^ "_has_extra_type_vars_on_rhs_", i), T); + else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T); in ctxt |> declare_term t'