src/Pure/Isar/locale.ML

   val extend = I;
   val merge = Name_Space.join_tables (K merge_locale);
 );
 
 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;
 
 fun the_locale thy name =

 (*** diagnostic commands and interfaces ***)
 
 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 =
   let
     val name = intern thy raw_name;