added syntax_name;
authorwenzelm
Sun, 05 Nov 2006 21:44:34 +0100
changeset 21181 13c3fdccdf0d
parent 21180 f27f12bcafb8
child 21182 747ff99b35ee
added syntax_name;
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 *)