src/Pure/Isar/attrib.ML
changeset 6846 f2380295d4dd
parent 6772 111845fce1b7
child 6874 747f656e04ec
--- a/src/Pure/Isar/attrib.ML	Mon Jun 28 21:38:50 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Jun 28 21:41:02 1999 +0200
@@ -61,10 +61,11 @@
   fun print _ ({space, attrs}) =
     let
       fun prt_attr (name, ((_, comment), _)) = Pretty.block
-        [Pretty.str (NameSpace.cond_extern space name ^ ":"), Pretty.brk 2, Pretty.str comment];
+        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     in
       Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
-      Pretty.writeln (Pretty.big_list "attributes:" (map prt_attr (Symtab.dest attrs)))
+      Pretty.writeln (Pretty.big_list "attributes:"
+        (map prt_attr (NameSpace.cond_extern_table space attrs)))
     end;
 end;