# HG changeset patch
# User wenzelm
# Date 1194470413 -3600
# Node ID db0365e89f5a7fb5644d5d846c971782dd0b9288
# Parent  0c509c33cfb77236cea0be936d84292d0e162f51
ProofContext.read_const';

diff -r 0c509c33cfb7 -r db0365e89f5a src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Nov 07 22:20:12 2007 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Nov 07 22:20:13 2007 +0100
@@ -241,7 +241,7 @@
 val _ = inline_antiq "type_syntax" (type_ true);
 
 fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
-  #1 (Term.dest_Const (Consts.read_const (ProofContext.consts_of ctxt) c))
+  #1 (Term.dest_Const (ProofContext.read_const' ctxt c))
   |> syn ? ProofContext.const_syntax_name ctxt
   |> ML_Syntax.print_string);