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);