Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/proof_context.ML
changeset 25133 b933700f0384
parent 25097 796190c7918d
child 25159 1822da5446bc 
--- 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
isabelle