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