diff -r c3681b9e060f -r 4873054cd1fc src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -104,7 +104,7 @@
           Pretty.block
             (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   in
-    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
+    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table ctxt attribs))]
     |> Pretty.chunks |> Pretty.writeln
   end;
 
@@ -337,7 +337,9 @@
           Pretty.brk 1, Pretty.str (Config.print_value value)]
       end;
     val space = attribute_space ctxt;
-    val configs = Name_Space.extern_table' ctxt space (Configs.get (Proof_Context.theory_of ctxt));
+    val configs =
+      Name_Space.markup_entries ctxt space
+        (Symtab.dest (Configs.get (Proof_Context.theory_of ctxt)));
   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;