# HG changeset patch
# User wenzelm
# Date 1085167214 -7200
# Node ID 69cafc301399f93307e4eb58d68f36ecf256f885
# Parent  5bb4bbdb6529a01213aed4799adb1bee0470bdbb
Sign.certify_tyname;

diff -r 5bb4bbdb6529 -r 69cafc301399 src/Pure/Isar/isar_thy.ML
--- 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 =