# HG changeset patch
# User wenzelm
# Date 1193138957 -7200
# Node ID 1822da5446bc2e17779f226f5f6d29259818152b
# Parent  271e499f2d033adde0c100ef04b244d19a437c2c
added XCONST syntax (keeps original spelling of const);

diff -r 271e499f2d03 -r 1822da5446bc src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Oct 23 13:29:16 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 23 13:29:17 2007 +0200
@@ -980,19 +980,29 @@
 
 (* authentic constants *)
 
-fun context_const_ast_tr ctxt [Syntax.Variable c] =
+local
+
+fun const_ast_tr intern ctxt [Syntax.Variable c] =
       let
         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 (const_syntax_name ctxt c') end
-  | context_const_ast_tr _ asts = raise Syntax.AST ("const_ast_tr", asts);
+        val d = if intern then const_syntax_name ctxt c' else c;
+      in Syntax.Constant d end
+  | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
+
+in
 
 val _ = Context.add_setup
  (Sign.add_syntax
    [("_context_const", "id => 'a", Delimfix "CONST _"),
-    ("_context_const", "longid => 'a", Delimfix "CONST _")] #>
-  Sign.add_advanced_trfuns ([("_context_const", context_const_ast_tr)], [], [], []));
+    ("_context_const", "longid => 'a", Delimfix "CONST _"),
+    ("_context_xconst", "id => 'a", Delimfix "XCONST _"),
+    ("_context_xconst", "longid => 'a", Delimfix "XCONST _")] #>
+  Sign.add_advanced_trfuns
+    ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], []));
+
+end;
 
 
 (* notation *)