src/Pure/Isar/element.ML

--- a/src/Pure/Isar/element.ML	Thu Nov 13 01:31:20 2008 +0100
+++ b/src/Pure/Isar/element.ML	Thu Nov 13 14:19:07 2008 +0100
@@ -159,8 +159,7 @@
 
 fun pretty_name_atts ctxt (binding, atts) sep =
   let
-    val name = NameSpace.implode
-      (map fst (Name.prefix_of binding) @ [Name.name_of binding]);
+    val name = Name.output binding;
   in if name = "" andalso null atts then []
     else [Pretty.block
       (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]