1.1 --- a/src/Pure/General/name_space.ML	Sun Mar 18 08:57:45 2012 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Sun Mar 18 10:28:31 2012 +0100
     1.3 @@ -48,8 +48,8 @@
     1.4    val qualified_path: bool -> binding -> naming -> naming
     1.5    val transform_binding: naming -> binding -> binding
     1.6    val full_name: naming -> binding -> string
     1.7 +  val alias: naming -> binding -> string -> T -> T
     1.8    val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
     1.9 -  val alias: naming -> binding -> string -> T -> T
    1.10    type 'a table = T * 'a Symtab.table
    1.11    val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
    1.12    val get: 'a table -> string -> 'a
    1.13 @@ -330,6 +330,26 @@
    1.14    in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
    1.15  
    1.16  
    1.17 +(* alias *)
    1.18 +
    1.19 +fun alias naming binding name space =
    1.20 +  let
    1.21 +    val (accs, accs') = accesses naming binding;
    1.22 +    val space' = space
    1.23 +      |> fold (add_name name) accs
    1.24 +      |> map_name_space (fn (kind, internals, entries) =>
    1.25 +        let
    1.26 +          val _ = Symtab.defined entries name orelse error (undefined kind name);
    1.27 +          val entries' = entries
    1.28 +            |> Symtab.map_entry name (fn (externals, entry) =>
    1.29 +              (Library.merge (op =) (externals, accs'), entry))
    1.30 +        in (kind, internals, entries') end);
    1.31 +  in space' end;
    1.32 +
    1.33 +
    1.34 +
    1.35 +(** entry definition **)
    1.36 +
    1.37  (* declaration *)
    1.38  
    1.39  fun new_entry strict (name, (externals, entry)) =
    1.40 @@ -364,25 +384,7 @@
    1.41    in (name, space') end;
    1.42  
    1.43  
    1.44 -(* alias *)
    1.45 -
    1.46 -fun alias naming binding name space =
    1.47 -  let
    1.48 -    val (accs, accs') = accesses naming binding;
    1.49 -    val space' = space
    1.50 -      |> fold (add_name name) accs
    1.51 -      |> map_name_space (fn (kind, internals, entries) =>
    1.52 -        let
    1.53 -          val _ = Symtab.defined entries name orelse error (undefined kind name);
    1.54 -          val entries' = entries
    1.55 -            |> Symtab.map_entry name (fn (externals, entry) =>
    1.56 -              (Library.merge (op =) (externals, accs'), entry))
    1.57 -        in (kind, internals, entries') end);
    1.58 -  in space' end;
    1.59 -
    1.60 -
    1.61 -
    1.62 -(** name space coupled with symbol table **)
    1.63 +(* definition in symbol table *)
    1.64  
    1.65  type 'a table = T * 'a Symtab.table;
    1.66