print_theory: omit name spaces; NameSpace.extern_table;
authorwenzelm
Thu Jun 09 12:03:21 2005 +0200 (2005-06-09)
changeset 16334b773132e3715
parent 16333 490d77820631
child 16335 37aabcf75ee1
print_theory: omit name spaces; NameSpace.extern_table;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Thu Jun 09 12:03:20 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Jun 09 12:03:21 2005 +0200
     1.3 @@ -224,21 +224,19 @@
     1.4  
     1.5  
     1.6      val {sign = _, defs, axioms, oracles, parents = _, ancestors = _} = Theory.rep_theory thy;
     1.7 -    val {self = _, tsig, consts, naming, 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.extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2;
    1.14      val cnsts = Sign.extern_table sg Sign.constK consts;
    1.15      val finals = Sign.extern_table sg Sign.constK (Defs.finals defs);
    1.16 -    val axms = Sign.extern_table sg Theory.axiomK axioms;
    1.17 -    val oras = Sign.extern_table sg Theory.oracleK oracles;
    1.18 +    val axms = NameSpace.extern_table axioms;
    1.19 +    val oras = NameSpace.extern_table oracles;
    1.20    in
    1.21      [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
    1.22        Pretty.strs ("data:" :: Sign.data_kinds data),
    1.23        Pretty.strs ["name prefix:", NameSpace.path_of naming],
    1.24 -      Pretty.big_list "name spaces:" (map pretty_name_space spcs),
    1.25        Pretty.big_list "classes:" (map pretty_classrel (Graph.dest classes)),
    1.26        pretty_default default,
    1.27        pretty_witness witness,