# HG changeset patch
# User wenzelm
# Date 1152035399 -7200
# Node ID 8d9d770e1f060725c23824eed2108c4a3cf5b4ab
# Parent  8f9e6255108ec079c4c280ff98e63d326470ae3e
add_abbrevs/polymorphic: Variable.exportT_terms avoids over-generalization;

diff -r 8f9e6255108e -r 8d9d770e1f06 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 04 19:49:58 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 04 19:49:59 2006 +0200
@@ -880,7 +880,8 @@
   let
     val ([(c, _, mx)], _) = cert_vars [(raw_c, NONE, raw_mx)] ctxt;
     val c' = Syntax.constN ^ full_name ctxt c;
-    val [t] = Variable.polymorphic ctxt [cert_term (ctxt |> expand_abbrevs false) raw_t];
+    val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t;
+    val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val T = Term.fastype_of t;
     val _ =
       if null (Variable.hidden_polymorphism t T) then ()