src/Pure/Isar/locale.ML

   (case get_locale thy name of
     SOME (Loc loc) => loc
   | NONE => error ("Unknown locale " ^ quote name));
 
 fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
-  thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
+  thy |> Locales.map (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
     (binding,
       mk_locale ((parameters, spec, intros, axioms),
         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
           (map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies,
             Inttab.empty)))) #> snd);