src/Pure/General/name_space.ML

   val mandatory_path: string -> naming -> naming
   val qualified_path: bool -> binding -> naming -> naming
   val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
   val declare: bool -> naming -> binding -> T -> string * T
+  val alias: naming -> binding -> string -> T -> T
   type 'a table = T * 'a Symtab.table
   val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
   val empty_table: string -> 'a table
   val merge_tables: 'a table * 'a table -> 'a table
   val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->

 
 
 (* datatype entry *)
 
 type entry =
- {externals: xstring list,
-  concealed: bool,
+ {concealed: bool,
   group: serial option,
   theory_name: string,
   pos: Position.T,
   id: serial};
 

 
 datatype T =
   Name_Space of
    {kind: string,
     internals: (string list * string list) Symtab.table,  (*visible, hidden*)
-    entries: entry Symtab.table};
+    entries: (xstring list * entry) Symtab.table};        (*externals, entry*)
 
 fun make_name_space (kind, internals, entries) =
   Name_Space {kind = kind, internals = internals, entries = entries};
 
 fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =

 fun kind_of (Name_Space {kind, ...}) = kind;
 
 fun the_entry (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
-  | SOME {concealed, group, theory_name, pos, id, ...} =>
-      {concealed = concealed, group = group, theory_name = theory_name, pos = pos, id = id});
+  | SOME (_, entry) => entry);
 
 fun is_concealed space name = #concealed (the_entry space name);
 
 
 (* name accesses *)

   | SOME ([], name' :: _) => (hidden name', true));
 
 fun get_accesses (Name_Space {entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => [name]
-  | SOME {externals, ...} => externals);
+  | SOME (externals, _) => externals);
 
 fun valid_accesses (Name_Space {internals, ...}) name =
   Symtab.fold (fn (xname, (names, _)) =>
     if not (null names) andalso hd names = name then cons xname else I) internals [];
 

       (K (fn ((names1, names1'), (names2, names2')) =>
         if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
         then raise Symtab.SAME
         else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
     val entries' = (entries1, entries2) |> Symtab.join
-      (fn name => fn (entry1, entry2) =>
+      (fn name => fn ((_, entry1), (_, entry2)) =>
         if #id entry1 = #id entry2 then raise Symtab.SAME
         else err_dup kind' (name, entry1) (name, entry2));
   in make_name_space (kind', internals', entries') end;
 
 

   in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
 
 
 (* declaration *)
 
-fun new_entry strict entry =
+fun new_entry strict (name, (externals, entry)) =
   map_name_space (fn (kind, internals, entries) =>
     let
       val entries' =
-        (if strict then Symtab.update_new else Symtab.update) entry entries
+        (if strict then Symtab.update_new else Symtab.update) (name, (externals, entry)) entries
           handle Symtab.DUP dup =>
-            err_dup kind (dup, the (Symtab.lookup entries dup)) entry;
+            err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
     in (kind, internals, entries') end);
 
 fun declare strict naming binding space =
   let
     val Naming {group, theory_name, ...} = naming;

 
     val name = Long_Name.implode (map fst spec);
     val _ = name = "" andalso err_bad binding;
 
     val entry =
-     {externals = accs',
-      concealed = concealed,
+     {concealed = concealed,
       group = group,
       theory_name = theory_name,
       pos = Position.default (Binding.pos_of binding),
       id = serial ()};
-    val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
+    val space' = space
+      |> fold (add_name name) accs
+      |> new_entry strict (name, (accs', entry));
   in (name, space') end;
+
+
+(* alias *)
+
+fun alias naming binding name space =
+  let
+    val (accs, accs') = accesses naming binding;
+    val space' = space
+      |> fold (add_name name) accs
+      |> map_name_space (fn (kind, internals, entries) =>
+        let
+          val _ = Symtab.defined entries name orelse
+            error ("Undefined " ^ kind ^ " " ^ quote name);
+          val entries' = entries
+            |> Symtab.map_entry name (fn (externals, entry) =>
+              (Library.merge (op =) (externals, accs'), entry))
+        in (kind, internals, entries') end);
+  in space' end;
 
 
 
 (** name spaces coupled with symbol tables **)