# HG changeset patch
# User wenzelm
# Date 1172696741 -3600
# Node ID b711c2ad750759bad9a1b27521008455d02c2050
# Parent  823f7bee42dfbb47504f2bf0d538cb4fdd3cc7a5
added @{const_name}, @{const_syntax};

diff -r 823f7bee42df -r b711c2ad7507 NEWS
--- a/NEWS	Wed Feb 28 16:35:00 2007 +0100
+++ b/NEWS	Wed Feb 28 22:05:41 2007 +0100
@@ -769,6 +769,8 @@
 ML {* @{cprop "x == y"} *}
 ML {* @{thm asm_rl} *}
 ML {* @{thms asm_rl} *}
+ML {* @{const_name c} *}
+ML {* @{const_syntax c} *}
 ML {* @{context} *}
 ML {* @{theory} *}
 ML {* @{theory Pure} *}
diff -r 823f7bee42df -r b711c2ad7507 src/Pure/Thy/ml_context.ML
--- a/src/Pure/Thy/ml_context.ML	Wed Feb 28 16:35:00 2007 +0100
+++ b/src/Pure/Thy/ml_context.ML	Wed Feb 28 22:05:41 2007 +0100
@@ -206,6 +206,15 @@
     "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
 
 
+fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
+  #1 (Term.dest_Const (Consts.read_const (ProofContext.consts_of ctxt) c))
+  |> syn ? ProofContext.const_syntax_name ctxt
+  |> ML_Syntax.print_string);
+
+val _ = inline_antiq "const_name" (const false);
+val _ = inline_antiq "const_syntax" (const true);
+
+
 
 (** fact references **)