# HG changeset patch
# User wenzelm
# Date 1162759474 -3600
# Node ID 13c3fdccdf0d347bd1df20e956422acbe881cb1b
# Parent  f27f12bcafb8c00ecbe94df3e32b82ece0ae5778
added syntax_name;

diff -r f27f12bcafb8 -r 13c3fdccdf0d src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Nov 05 21:44:33 2006 +0100
+++ b/src/Pure/consts.ML	Sun Nov 05 21:44:34 2006 +0100
@@ -22,6 +22,7 @@
   val extern: T -> string -> xstring
   val extern_early: T -> string -> xstring
   val syntax: T -> string * mixfix -> string * typ * mixfix
+  val syntax_name: T -> string -> string
   val read_const: T -> string -> term
   val certify: Pretty.pp -> Type.tsig -> T -> term -> term          (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
@@ -123,6 +124,8 @@
     val c' = if authentic then Syntax.constN ^ c else NameSpace.base c;
   in (c', T, mx) end;
 
+fun syntax_name consts c = #1 (syntax consts (c, NoSyn));
+
 
 (* read_const *)