# HG changeset patch
# User wenzelm
# Date 1002820920 -7200
# Node ID 5341e38309e8b270bbe7d7614cd1608aa5499c1c
# Parent  49c14348a42b8818a33e8dc3c9d1e766982caf74
added certify_tyname;

diff -r 49c14348a42b -r 5341e38309e8 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Oct 10 18:41:13 2001 +0200
+++ b/src/Pure/sign.ML	Thu Oct 11 19:22:00 2001 +0200
@@ -89,6 +89,7 @@
   val certify_typ_no_norm: sg -> typ -> typ
   val certify_tycon: sg -> string -> string
   val certify_tyabbr: sg -> string -> string
+  val certify_tyname: sg -> string -> string
   val certify_const: sg -> string -> string
   val certify_term: sg -> term -> term * typ * int
   val read_sort: sg -> string -> sort
@@ -615,6 +616,10 @@
   if is_some (Symtab.lookup (#abbrs (Type.rep_tsig (tsig_of sg)), c)) then c
   else raise TYPE ("Unknown type abbreviation " ^ quote c, [], []);
 
+fun certify_tyname sg c =
+  certify_tycon sg c handle TYPE _ => certify_tyabbr sg c handle TYPE _ =>
+    raise TYPE ("Unknown type name " ^ quote c, [], []);
+
 fun certify_const sg c =
   if is_some (const_type sg c) then c else raise TYPE ("Undeclared constant " ^ quote c, [], []);