# HG changeset patch
# User wenzelm
# Date 1332062911 -3600
# Node ID 3094745a41efa0045ec8a43a8c36c8d439a47395
# Parent  9435d419109a1e6d5d4566080bd73d923ec86e28
tuned structure;

diff -r 9435d419109a -r 3094745a41ef src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Mar 18 08:57:45 2012 +0100
+++ b/src/Pure/General/name_space.ML	Sun Mar 18 10:28:31 2012 +0100
@@ -48,8 +48,8 @@
   val qualified_path: bool -> binding -> naming -> naming
   val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
+  val alias: naming -> binding -> string -> T -> T
   val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
-  val alias: naming -> binding -> string -> T -> T
   type 'a table = T * 'a Symtab.table
   val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
   val get: 'a table -> string -> 'a
@@ -330,6 +330,26 @@
   in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) 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 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;
+
+
+
+(** entry definition **)
+
 (* declaration *)
 
 fun new_entry strict (name, (externals, entry)) =
@@ -364,25 +384,7 @@
   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 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 space coupled with symbol table **)
+(* definition in symbol table *)
 
 type 'a table = T * 'a Symtab.table;