NameSpace.dest_table avoids duplicated extern;
authorwenzelm
Thu Jul 14 19:28:28 2005 +0200 (2005-07-14)
changeset 16845bedf7b5fb781
parent 16844 60ab395e6da5
child 16846 bbebc68a7faf
NameSpace.dest_table avoids duplicated extern;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Thu Jul 14 19:28:26 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Jul 14 19:28:28 2005 +0200
     1.3 @@ -200,10 +200,9 @@
     1.4      val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
     1.5      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
     1.6  
     1.7 -    val clsses = NameSpace.extern_table (apsnd (Symtab.make o Graph.dest) classes);
     1.8 -    val tdecls = NameSpace.extern_table types;
     1.9 -    val arties = Symtab.dest arities
    1.10 -      |> Library.sort_wrt (NameSpace.extern (Sign.type_space thy) o #1);
    1.11 +    val clsses = NameSpace.dest_table (apsnd (Symtab.make o Graph.dest) classes);
    1.12 +    val tdecls = NameSpace.dest_table types;
    1.13 +    val arties = NameSpace.dest_table (Sign.type_space thy, arities);
    1.14      val cnsts = NameSpace.extern_table consts;
    1.15      val finals = NameSpace.extern_table (#1 consts, Defs.finals defs);
    1.16      val axms = NameSpace.extern_table axioms;