# HG changeset patch
# User wenzelm
# Date 1117533198 -7200
# Node ID 549fff1d0fc69317137bfdd79ed1481c294960ad
# Parent  3ba9eb7ea3667c69aa774c1bca2331a9de2476b8
renamed cond_extern to extern;
NameSpace.path_of naming;

diff -r 3ba9eb7ea366 -r 549fff1d0fc6 src/Pure/display.ML
--- a/src/Pure/display.ML	Tue May 31 11:53:17 2005 +0200
+++ b/src/Pure/display.ML	Tue May 31 11:53:18 2005 +0200
@@ -225,20 +225,20 @@
 
     val {sign = _, const_deps = _, final_consts, axioms, oracles,
       parents = _, ancestors = _} = Theory.rep_theory thy;
-    val {self = _, tsig, consts, path, 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.cond_extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2;
-    val cnsts = Sign.cond_extern_table sg Sign.constK consts;
-    val finals = Sign.cond_extern_table sg Sign.constK final_consts;
-    val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
-    val oras = Sign.cond_extern_table sg Theory.oracleK oracles;
+      (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 final_consts;
+    val axms = Sign.extern_table sg Theory.axiomK axioms;
+    val oras = Sign.extern_table sg Theory.oracleK oracles;
   in
     [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
       Pretty.strs ("data:" :: Sign.data_kinds data),
-      Pretty.strs ["name prefix:", NameSpace.pack (getOpt (path,["-"]))],
+      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,