added certify_tyname;
authorwenzelm
Thu Oct 11 19:22:00 2001 +0200 (2001-10-11)
changeset 117205341e38309e8
parent 11719 49c14348a42b
child 11721 0d60622b668f
added certify_tyname;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Wed Oct 10 18:41:13 2001 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Oct 11 19:22:00 2001 +0200
     1.3 @@ -89,6 +89,7 @@
     1.4    val certify_typ_no_norm: sg -> typ -> typ
     1.5    val certify_tycon: sg -> string -> string
     1.6    val certify_tyabbr: sg -> string -> string
     1.7 +  val certify_tyname: sg -> string -> string
     1.8    val certify_const: sg -> string -> string
     1.9    val certify_term: sg -> term -> term * typ * int
    1.10    val read_sort: sg -> string -> sort
    1.11 @@ -615,6 +616,10 @@
    1.12    if is_some (Symtab.lookup (#abbrs (Type.rep_tsig (tsig_of sg)), c)) then c
    1.13    else raise TYPE ("Unknown type abbreviation " ^ quote c, [], []);
    1.14  
    1.15 +fun certify_tyname sg c =
    1.16 +  certify_tycon sg c handle TYPE _ => certify_tyabbr sg c handle TYPE _ =>
    1.17 +    raise TYPE ("Unknown type name " ^ quote c, [], []);
    1.18 +
    1.19  fun certify_const sg c =
    1.20    if is_some (const_type sg c) then c else raise TYPE ("Undeclared constant " ^ quote c, [], []);
    1.21