src/Pure/Isar/locale.ML

 (
   type T = NameSpace.T * locale Symtab.table;
     (* 1st entry: locale namespace,
        2nd entry: locales of the theory *)
 
-  val empty = (NameSpace.empty, Symtab.empty);
+  val empty = NameSpace.empty_table;
   val copy = I;
   val extend = I;
 
   fun join_locales _
     ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale,

        (Library.merge (eq_snd (op =)) (decls1, decls1'),
         Library.merge (eq_snd (op =)) (decls2, decls2')),
       regs = merge_alists (op =) regs regs',
       intros = intros,
       dests = dests};
-  fun merge _ ((space1, locs1), (space2, locs2)) =
-    (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
+  fun merge _ = NameSpace.join_tables join_locales;
 );
 
 
 
 (** context data : registrations **)

 
 fun the_locale thy name = case get_locale thy name
  of SOME loc => loc
   | NONE => error ("Unknown locale " ^ quote name);
 
-fun register_locale name loc thy =
-  thy |> LocalesData.map (fn (space, locs) =>
-    (NameSpace.declare_base (Sign.naming_of thy) name space,
-      Symtab.update (name, loc) locs));
+fun register_locale bname loc thy =
+  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy)
+    (Binding.name bname, loc) #> snd);
 
 fun change_locale name f thy =
   let
     val {axiom, elems, params, decls, regs, intros, dests} =
         the_locale thy name;

     val loc_ctxt = thy'
       |> Sign.add_path bname
       |> Sign.no_base_names
       |> PureThy.note_thmss Thm.assumptionK facts' |> snd
       |> Sign.restore_naming thy'
-      |> register_locale name {axiom = axs',
+      |> register_locale bname {axiom = axs',
         elems = map (fn e => (e, stamp ())) elems'',
         params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
         decls = ([], []),
         regs = regs,
         intros = intros,