changeset 35262 | 9ea4445d2ccf |
parent 35255 | 2cb27605301f |
child 35361 | 4c7c849b70aa |
--- a/src/Pure/ML/ml_antiquote.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/ML/ml_antiquote.ML Sun Feb 21 22:35:02 2010 +0100 @@ -114,7 +114,7 @@ fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c)) - |> syn ? prefix Syntax.constN + |> syn ? Syntax.mark_const |> ML_Syntax.print_string); val _ = inline "const_name" (const false);