1.1 --- a/src/Pure/display.ML	Tue May 31 11:53:17 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Tue May 31 11:53:18 2005 +0200
     1.3 @@ -225,20 +225,20 @@
     1.4  
     1.5      val {sign = _, const_deps = _, final_consts, axioms, oracles,
     1.6        parents = _, ancestors = _} = Theory.rep_theory thy;
     1.7 -    val {self = _, tsig, consts, path, spaces, data} = Sign.rep_sg sg;
     1.8 +    val {self = _, tsig, consts, naming, spaces, data} = Sign.rep_sg sg;
     1.9      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
    1.10  
    1.11      val spcs = Library.sort_wrt #1 spaces;
    1.12      val tdecls = Symtab.dest types |> map (fn (t, (d, _)) =>
    1.13 -      (Sign.cond_extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2;
    1.14 -    val cnsts = Sign.cond_extern_table sg Sign.constK consts;
    1.15 -    val finals = Sign.cond_extern_table sg Sign.constK final_consts;
    1.16 -    val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
    1.17 -    val oras = Sign.cond_extern_table sg Theory.oracleK oracles;
    1.18 +      (Sign.extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2;
    1.19 +    val cnsts = Sign.extern_table sg Sign.constK consts;
    1.20 +    val finals = Sign.extern_table sg Sign.constK final_consts;
    1.21 +    val axms = Sign.extern_table sg Theory.axiomK axioms;
    1.22 +    val oras = Sign.extern_table sg Theory.oracleK oracles;
    1.23    in
    1.24      [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
    1.25        Pretty.strs ("data:" :: Sign.data_kinds data),
    1.26 -      Pretty.strs ["name prefix:", NameSpace.pack (getOpt (path,["-"]))],
    1.27 +      Pretty.strs ["name prefix:", NameSpace.path_of naming],
    1.28        Pretty.big_list "name spaces:" (map pretty_name_space spcs),
    1.29        Pretty.big_list "classes:" (map pretty_classrel (Graph.dest classes)),
    1.30        pretty_default default,