print_theory: omit name spaces; NameSpace.extern_table;

--- a/src/Pure/display.ML	Thu Jun 09 12:03:20 2005 +0200
+++ b/src/Pure/display.ML	Thu Jun 09 12:03:21 2005 +0200
@@ -224,21 +224,19 @@
 
 
     val {sign = _, defs, axioms, oracles, parents = _, ancestors = _} = Theory.rep_theory thy;
-    val {self = _, tsig, consts, naming, spaces, data} = Sign.rep_sg sg;
+    val {self = _, tsig, consts, naming, spaces = _, data} = Sign.rep_sg sg;
     val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
 
-    val spcs = Library.sort_wrt #1 spaces;
     val tdecls = Symtab.dest types |> map (fn (t, (d, _)) =>
       (Sign.extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2;
     val cnsts = Sign.extern_table sg Sign.constK consts;
     val finals = Sign.extern_table sg Sign.constK (Defs.finals defs);
-    val axms = Sign.extern_table sg Theory.axiomK axioms;
-    val oras = Sign.extern_table sg Theory.oracleK oracles;
+    val axms = NameSpace.extern_table axioms;
+    val oras = NameSpace.extern_table oracles;
   in
     [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
       Pretty.strs ("data:" :: Sign.data_kinds data),
       Pretty.strs ["name prefix:", NameSpace.path_of naming],
-      Pretty.big_list "name spaces:" (map pretty_name_space spcs),
       Pretty.big_list "classes:" (map pretty_classrel (Graph.dest classes)),
       pretty_default default,
       pretty_witness witness,