# HG changeset patch
# User wenzelm
# Date 954532583 -7200
# Node ID e86e49aa1631f5f702871d9e29b3fa4354e9b14a
# Parent  635dd6b130285341a502fba780e94d66b1dd911c
tuned;

diff -r 635dd6b13028 -r e86e49aa1631 src/Pure/Isar/proof_context.ML
--- 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'