src/Pure/consts.ML
changeset 21181 13c3fdccdf0d
parent 20734 8aa9590bd452
child 21205 dfe338ec9f9c
     1.1 --- a/src/Pure/consts.ML	Sun Nov 05 21:44:33 2006 +0100
     1.2 +++ b/src/Pure/consts.ML	Sun Nov 05 21:44:34 2006 +0100
     1.3 @@ -22,6 +22,7 @@
     1.4    val extern: T -> string -> xstring
     1.5    val extern_early: T -> string -> xstring
     1.6    val syntax: T -> string * mixfix -> string * typ * mixfix
     1.7 +  val syntax_name: T -> string -> string
     1.8    val read_const: T -> string -> term
     1.9    val certify: Pretty.pp -> Type.tsig -> T -> term -> term          (*exception TYPE*)
    1.10    val typargs: T -> string * typ -> typ list
    1.11 @@ -123,6 +124,8 @@
    1.12      val c' = if authentic then Syntax.constN ^ c else NameSpace.base c;
    1.13    in (c', T, mx) end;
    1.14  
    1.15 +fun syntax_name consts c = #1 (syntax consts (c, NoSyn));
    1.16 +
    1.17  
    1.18  (* read_const *)
    1.19