src/Pure/display.ML

     val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
     val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
     val {constants, constraints} = Consts.dest consts;
-    val extern_const = Name_Space.extern (#1 constants);
+    val extern_const = Name_Space.extern ctxt (#1 constants);
     val {classes, default, types, ...} = Type.rep_tsig tsig;
     val (class_space, class_algebra) = classes;
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
-    val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
-    val tdecls = Name_Space.dest_table types;
-    val arties = Name_Space.dest_table (Sign.type_space thy, arities);
+    val clsses = Name_Space.dest_table ctxt (class_space, Symtab.make (Graph.dest classes));
+    val tdecls = Name_Space.dest_table ctxt types;
+    val arties = Name_Space.dest_table ctxt (Sign.type_space thy, arities);
 
     fun prune_const c = not verbose andalso Consts.is_concealed consts c;
-    val cnsts = Name_Space.extern_table (#1 constants,
+    val cnsts = Name_Space.extern_table ctxt (#1 constants,
       Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 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 constraints;
-
-    val axms = Name_Space.extern_table axioms;
+    val cnstrs = Name_Space.extern_table ctxt constraints;
+
+    val axms = Name_Space.extern_table ctxt axioms;
 
     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
         (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
       |> sort_wrt (#1 o #1)

       Pretty.big_list "type arities:" (pretty_arities arties),
       Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
       Pretty.big_list "axioms:" (map pretty_axm axms),
-      Pretty.strs ("oracles:" :: Thm.extern_oracles thy),
+      Pretty.strs ("oracles:" :: Thm.extern_oracles ctxt),
       Pretty.big_list "definitions:"
         [pretty_finals reds0,
          Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
          Pretty.big_list "overloaded:" (map pretty_reduct reds2),
          Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]