diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -129,7 +129,8 @@
 
 (* pretty printing *)
 
-fun extern ctxt = Name_Space.extern ctxt (#1 (get_attributes (Context.Proof ctxt)));
+fun extern ctxt =
+  Name_Space.extern ctxt (Name_Space.space_of_table (get_attributes (Context.Proof ctxt)));
 
 fun pretty_attribs _ [] = []
   | pretty_attribs ctxt srcs =
@@ -139,12 +140,12 @@
 (* get attributes *)
 
 fun attribute_generic context =
-  let val (_, tab) = get_attributes context in
+  let val table = get_attributes context in
     fn src =>
       let val ((name, _), pos) = Args.dest_src src in
-        (case Symtab.lookup tab name of
+        (case Name_Space.lookup_key table name of
           NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos)
-        | SOME (att, _) => att src)
+        | SOME (_, (att, _)) => att src)
       end
   end;
 
@@ -349,8 +350,8 @@
         Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
           Pretty.brk 1, Pretty.str (Config.print_value value)]
       end;
-    val space = #1 (get_attributes (Context.Proof ctxt));
-    val configs = Name_Space.extern_table ctxt (space, Configs.get (Proof_Context.theory_of ctxt));
+    val space = Name_Space.space_of_table (get_attributes (Context.Proof ctxt));
+    val configs = Name_Space.extern_table' ctxt space (Configs.get (Proof_Context.theory_of ctxt));
   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;