1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Feb 21 21:41:29 2010 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Feb 21 22:35:02 2010 +0100
     1.3 @@ -988,7 +988,7 @@
     1.4  fun const_ast_tr intern ctxt [Syntax.Variable c] =
     1.5        let
     1.6          val Const (c', _) = read_const_proper ctxt c;
     1.7 -        val d = if intern then Syntax.constN ^ c' else c;
     1.8 +        val d = if intern then Syntax.mark_const c' else c;
     1.9        in Syntax.Constant d end
    1.10    | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
    1.11  
    1.12 @@ -1017,7 +1017,7 @@
    1.13  fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx))
    1.14    | const_syntax ctxt (Const (c, _), mx) =
    1.15        (case try (Consts.type_scheme (consts_of ctxt)) c of
    1.16 -        SOME T => SOME (false, (Syntax.constN ^ c, T, mx))
    1.17 +        SOME T => SOME (false, (Syntax.mark_const c, T, mx))
    1.18        | NONE => NONE)
    1.19    | const_syntax _ _ = NONE;
    1.20