tuned;

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