# HG changeset patch # User wenzelm # Date 1121362108 -7200 # Node ID bedf7b5fb78196a88363cabac881dd926101a2b0 # Parent 60ab395e6da5112623ffa7b7fcc50c23f39859f1 NameSpace.dest_table avoids duplicated extern; diff -r 60ab395e6da5 -r bedf7b5fb781 src/Pure/display.ML --- a/src/Pure/display.ML Thu Jul 14 19:28:26 2005 +0200 +++ b/src/Pure/display.ML Thu Jul 14 19:28:28 2005 +0200 @@ -200,10 +200,9 @@ val {naming, syn = _, tsig, consts} = Sign.rep_sg thy; val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig; - val clsses = NameSpace.extern_table (apsnd (Symtab.make o Graph.dest) classes); - val tdecls = NameSpace.extern_table types; - val arties = Symtab.dest arities - |> Library.sort_wrt (NameSpace.extern (Sign.type_space thy) o #1); + val clsses = NameSpace.dest_table (apsnd (Symtab.make o Graph.dest) classes); + val tdecls = NameSpace.dest_table types; + val arties = NameSpace.dest_table (Sign.type_space thy, arities); val cnsts = NameSpace.extern_table consts; val finals = NameSpace.extern_table (#1 consts, Defs.finals defs); val axms = NameSpace.extern_table axioms;