src/Pure/Isar/attrib.ML
changeset 42813 6c841fa92fa2
parent 42808 30870aee8a3f
child 43347 f18cf88453d6
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun May 15 16:40:24 2011 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun May 15 17:06:35 2011 +0200
     1.3 @@ -78,8 +78,9 @@
     1.4    let
     1.5      val ctxt = Proof_Context.init_global thy;
     1.6      val attribs = Attributes.get thy;
     1.7 -    fun prt_attr (name, (_, comment)) = Pretty.block
     1.8 -      [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     1.9 +    fun prt_attr (name, (_, "")) = Pretty.str name
    1.10 +      | prt_attr (name, (_, comment)) =
    1.11 +          Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.12    in
    1.13      [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
    1.14      |> Pretty.chunks |> Pretty.writeln