# HG changeset patch
# User wenzelm
# Date 1118311413 -7200
# Node ID baa7b5324fc1ba7fd62a6110a9c0514544bc0746
# Parent  b035482bed0226316a3261fa48c72a3109ea6530
NameSpace.extern_table;
ProofContext.extern_thm;

diff -r b035482bed02 -r baa7b5324fc1 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Jun 09 12:03:32 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Jun 09 12:03:33 2005 +0200
@@ -343,7 +343,7 @@
      Symtab.join (SOME o Registrations.join) (regs1, regs2));
 
   fun print _ (space, locs, _) =
-    Pretty.strs ("locales:" :: map (NameSpace.extern space o #1) (Symtab.dest locs))
+    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
     |> Pretty.writeln;
 end;
 
@@ -1486,7 +1486,7 @@
       | prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
     fun prt_cst (x, T) = Pretty.block [Pretty.str (x ^ " ::"), prt_typ T];
 
-    fun prt_name name = Pretty.str (ProofContext.extern ctxt name);
+    fun prt_name name = Pretty.str (ProofContext.extern_thm ctxt name);
     fun prt_name_atts (name, atts) =
       if name = "" andalso null atts then []
       else [Pretty.block (Pretty.breaks (prt_name name :: prt_atts atts @ [Pretty.str ":"]))];