Sign.certify_tyname;

--- a/src/Pure/Isar/isar_thy.ML	Fri May 21 21:19:47 2004 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Fri May 21 21:20:14 2004 +0200
@@ -168,8 +168,7 @@
 
 val kinds =
  [(Sign.classK, can o Sign.certify_class),
-  (Sign.typeK, fn sg => fn c =>
-    can (Sign.certify_tycon sg) c orelse can (Sign.certify_tyabbr sg) c),
+  (Sign.typeK, can o Sign.certify_tyname),
   (Sign.constK, can o Sign.certify_const)];
 
 fun gen_hide intern (kind, xnames) thy =