# HG changeset patch
# User wenzelm
# Date 973880266 -3600
# Node ID 088aa7bd3154a15f8326d8dd09ec2407878f22d5
# Parent  da7d0e28f746906e2752e9a95045d20cfcb5e4a1
hide_space(_i): use Sign.certify_tycon, Sign.certify_tyabbr, Sign.certify_const;

diff -r da7d0e28f746 -r 088aa7bd3154 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Nov 10 19:15:38 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Nov 10 19:17:46 2000 +0100
@@ -208,11 +208,10 @@
 local
 
 val kinds =
- [(Sign.classK, fn sg => fn c => c mem Sign.classes sg),
+ [(Sign.classK, can o Sign.certify_class),
   (Sign.typeK, fn sg => fn c =>
-    let val {tycons, abbrs, ...} = Type.rep_tsig (Sign.tsig_of sg)
-    in is_some (Symtab.lookup (tycons, c)) orelse is_some (Symtab.lookup (abbrs, c)) end),
-  (Sign.constK, is_some oo Sign.const_type)];
+    can (Sign.certify_tycon sg) c orelse can (Sign.certify_tyabbr sg) c),
+  (Sign.constK, can o Sign.certify_const)];
 
 fun gen_hide intern ((kind, xnames), comment_ignore) thy =
   (case assoc (kinds, kind) of