src/Pure/ML/ml_antiquote.ML
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);