diff -r c3681b9e060f -r 4873054cd1fc src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/display.ML	Tue Mar 11 14:28:39 2014 +0100
@@ -157,22 +157,24 @@
     val arities = Sorts.arities_of class_algebra;
 
     val clsses =
-      Name_Space.dest_table' ctxt class_space
-        (Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)))
+      Name_Space.extern_entries ctxt class_space
+        (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
       |> map (apfst #1);
-    val tdecls = Name_Space.dest_table ctxt types |> map (apfst #1);
-    val arties = Name_Space.dest_table' ctxt (Type.type_space tsig) arities |> map (apfst #1);
+    val tdecls = Name_Space.extern_table ctxt types |> map (apfst #1);
+    val arties =
+      Name_Space.extern_entries ctxt (Type.type_space tsig) (Symtab.dest arities)
+      |> map (apfst #1);
 
     fun prune_const c = not verbose andalso Consts.is_concealed consts c;
     val cnsts =
-      Name_Space.extern_table' ctxt const_space
-        (Symtab.make (filter_out (prune_const o fst) (Symtab.dest constants)));
+      Name_Space.markup_entries ctxt const_space
+        (filter_out (prune_const o fst) (Symtab.dest constants));
 
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
-    val cnstrs = Name_Space.extern_table' ctxt const_space constraints;
+    val cnstrs = Name_Space.markup_entries ctxt const_space (Symtab.dest constraints);
 
-    val axms = Name_Space.extern_table ctxt (Theory.axiom_table thy);
+    val axms = Name_Space.markup_table ctxt (Theory.axiom_table thy);
 
     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       |> map (fn (lhs, rhs) =>