src/Pure/ML/ml_context.ML

 
 val _ = inline_antiq "type_name" (type_ false);
 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 (ProofContext.read_const' ctxt c))
+  #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
   |> syn ? ProofContext.const_syntax_name ctxt
   |> ML_Syntax.print_string);
 
 val _ = inline_antiq "const_name" (const false);
 val _ = inline_antiq "const_syntax" (const true);