context_const_ast_tr: proper const_syntax_name (cf. @{const_syntax});
authorwenzelm
Sun, 21 Oct 2007 14:21:54 +0200
changeset 25133 b933700f0384
parent 25132 dffe405b090d
child 25134 3d4953e88449
context_const_ast_tr: proper const_syntax_name (cf. @{const_syntax});
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