src/Pure/ML/ml_context.ML

--- a/src/Pure/ML/ml_context.ML	Fri Mar 14 08:52:52 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Fri Mar 14 08:52:53 2008 +0100
@@ -257,8 +257,7 @@
     >> (fn ((ctxt, c), Ts) =>
       let
         val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c);
-        val T = Consts.instance (ProofContext.consts_of ctxt) (c, Ts);
-      in ML_Syntax.atomic (ML_Syntax.print_term (Const (c, T))) end));
+      in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
 
 in val _ = () end;