--- a/src/Pure/Isar/element.ML Mon Nov 10 19:42:20 2008 +0100
+++ b/src/Pure/Isar/element.ML Mon Nov 10 19:42:21 2008 +0100
@@ -158,8 +158,10 @@
map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
fun pretty_name_atts ctxt (binding, atts) sep =
- let val name = Name.name_of binding in
- if name = "" andalso null atts then []
+ let
+ val name = NameSpace.implode
+ (map fst (Name.prefix_of binding) @ [Name.name_of binding]);
+ in if name = "" andalso null atts then []
else [Pretty.block
(Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
end;