src/Pure/display.ML
changeset 33158 6e3dc0ba2b06
parent 33095 bbd52d2f8696
child 33173 b8ca12f6681a
     1.1 --- a/src/Pure/display.ML	Sun Oct 25 12:27:21 2009 +0100
     1.2 +++ b/src/Pure/display.ML	Sun Oct 25 13:18:35 2009 +0100
     1.3 @@ -188,8 +188,7 @@
     1.4      val tdecls = Name_Space.dest_table types;
     1.5      val arties = Name_Space.dest_table (Sign.type_space thy, arities);
     1.6  
     1.7 -    fun prune_const c = not verbose andalso
     1.8 -      member (op =) (Consts.the_tags consts c) Markup.property_internal;
     1.9 +    fun prune_const c = not verbose andalso Consts.is_concealed consts c;
    1.10      val cnsts = Name_Space.extern_table (#1 constants,
    1.11        Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
    1.12