--- a/src/Pure/display.ML Sun Oct 25 12:27:21 2009 +0100
+++ b/src/Pure/display.ML Sun Oct 25 13:18:35 2009 +0100
@@ -188,8 +188,7 @@
val tdecls = Name_Space.dest_table types;
val arties = Name_Space.dest_table (Sign.type_space thy, arities);
- fun prune_const c = not verbose andalso
- member (op =) (Consts.the_tags consts c) Markup.property_internal;
+ fun prune_const c = not verbose andalso Consts.is_concealed consts c;
val cnsts = Name_Space.extern_table (#1 constants,
Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));