author | wenzelm |
Thu, 08 Nov 2007 14:51:31 +0100 | |
changeset 25346 | 7f2e3292e3dd |
parent 25345 | dd5b851f8ef0 |
child 25347 | 297e2520ee82 |
--- a/src/Pure/ML/ml_context.ML Thu Nov 08 14:51:30 2007 +0100 +++ b/src/Pure/ML/ml_context.ML Thu Nov 08 14:51:31 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 (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);