# HG changeset patch
# User wenzelm
# Date 1192969314 -7200
# Node ID b933700f0384ccd5c89dfa4c623d72b3355cd2ea
# Parent  dffe405b090deb3c2bc9d334b8e9c980068e6e56
context_const_ast_tr: proper const_syntax_name (cf. @{const_syntax});

diff -r dffe405b090d -r b933700f0384 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Oct 21 14:21:53 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Oct 21 14:21:54 2007 +0200
@@ -985,7 +985,7 @@
         val consts = consts_of ctxt;
         val c' = Consts.intern consts c;
         val _ = Consts.the_constraint consts c' handle TYPE (msg, _, _) => error msg;
-      in Syntax.Constant (Syntax.constN ^ c') end
+      in Syntax.Constant (const_syntax_name ctxt c') end
   | context_const_ast_tr _ asts = raise Syntax.AST ("const_ast_tr", asts);
 
 val _ = Context.add_setup