--- a/src/Pure/Isar/locale.ML Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Isar/locale.ML Sat Apr 16 13:48:45 2011 +0200
@@ -162,7 +162,7 @@
);
val intern = Name_Space.intern o #1 o Locales.get;
-val extern = Name_Space.extern o #1 o Locales.get;
+fun extern thy = Name_Space.extern (ProofContext.init_global thy) (#1 (Locales.get thy));
val get_locale = Symtab.lookup o #2 o Locales.get;
val defined = Symtab.defined o #2 o Locales.get;
@@ -630,7 +630,8 @@
val all_locales = Symtab.keys o snd o Locales.get;
fun print_locales thy =
- Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
+ Pretty.strs ("locales:" ::
+ map #1 (Name_Space.extern_table (ProofContext.init_global thy) (Locales.get thy)))
|> Pretty.writeln;
fun print_locale thy show_facts raw_name =