src/Pure/sign.ML
changeset 14700 2f885b7e5ba7
parent 14688 edb7dacde656
child 14784 e65d77313a94
     1.1 --- a/src/Pure/sign.ML	Sat May 01 22:28:51 2004 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon May 03 23:22:17 2004 +0200
     1.3 @@ -61,6 +61,7 @@
     1.4    val extern: sg -> string -> string -> xstring
     1.5    val cond_extern: sg -> string -> string -> xstring
     1.6    val cond_extern_table: sg -> string -> 'a Symtab.table -> (xstring * 'a) list
     1.7 +  val extern_typ: sg -> typ -> typ
     1.8    val intern_class: sg -> xclass -> class
     1.9    val intern_tycon: sg -> xstring -> string
    1.10    val intern_const: sg -> xstring -> string
    1.11 @@ -551,6 +552,9 @@
    1.12    val cond_extern = cond_extrn o spaces_of;
    1.13    fun cond_extern_table sg = cond_extrn_table (spaces_of sg);
    1.14  
    1.15 +  fun extern_typ (sg as Sg (_, {spaces, ...})) T =
    1.16 +       if ! NameSpace.long_names then T else extrn_typ spaces T;
    1.17 +
    1.18    val intern_class = intrn_class o spaces_of;
    1.19    val intern_sort = intrn_sort o spaces_of;
    1.20    val intern_typ = intrn_typ o spaces_of;
    1.21 @@ -596,9 +600,8 @@
    1.22  
    1.23  fun pretty_term sg = pretty_term' (syn_of sg) sg;
    1.24  
    1.25 -fun pretty_typ (sg as Sg (_, {spaces, ...})) T =
    1.26 -  Syntax.pretty_typ (syn_of sg)
    1.27 -    (if ! NameSpace.long_names then T else extrn_typ spaces T);
    1.28 +fun pretty_typ sg T =
    1.29 +  Syntax.pretty_typ (syn_of sg) (extern_typ sg T);
    1.30  
    1.31  fun pretty_sort (sg as Sg (_, {spaces, ...})) S =
    1.32    Syntax.pretty_sort (syn_of sg)