src/Pure/Isar/element.ML
changeset 28733 18ffcbf1b3ae
parent 28084 a05ca48ef263
child 28737 8cbb7cfcfb5b
--- 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;