1.1 --- a/src/Pure/ML/ml_context.ML	Thu Nov 08 14:51:30 2007 +0100
     1.2 +++ b/src/Pure/ML/ml_context.ML	Thu Nov 08 14:51:31 2007 +0100
     1.3 @@ -241,7 +241,7 @@
     1.4  val _ = inline_antiq "type_syntax" (type_ true);
     1.5  
     1.6  fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
     1.7 -  #1 (Term.dest_Const (ProofContext.read_const' ctxt c))
     1.8 +  #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
     1.9    |> syn ? ProofContext.const_syntax_name ctxt
    1.10    |> ML_Syntax.print_string);
    1.11