--- 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 *)