eliminated internal stamp equality, replaced by bare-metal pointer_eq;
misc tuning and polishing;

--- a/src/Pure/General/name_space.ML	Tue Mar 03 21:49:34 2009 +0100
+++ b/src/Pure/General/name_space.ML	Tue Mar 03 21:53:52 2009 +0100
@@ -3,7 +3,6 @@
 
 Generic name spaces with declared and hidden entries.  Unknown names
 are considered global; no support for absolute addressing.
-Cf. Pure/General/binding.ML
 *)
 
 type xstring = string;    (*external names*)
@@ -48,12 +47,11 @@
   val qualified_names: naming -> naming
   val sticky_prefix: string -> naming -> naming
   type 'a table = T * 'a Symtab.table
+  val bind: naming -> binding * 'a -> 'a table -> string * 'a table       (*exception Symtab.DUP*)
   val empty_table: 'a table
-  val bind: naming -> binding * 'a
-    -> 'a table -> string * 'a table (*exception Symtab.DUP*)
-  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
-  val join_tables: (string -> 'a * 'a -> 'a)
-    -> 'a table * 'a table -> 'a table
+  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table  (*exception Symtab.DUP*)
+  val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) ->
+    'a table * 'a table -> 'a table                                       (*exception Symtab.DUP*)
   val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
 end;
@@ -124,28 +122,28 @@
 
 datatype T =
   NameSpace of
-    ((string list * string list) * stamp) Symtab.table *   (*internals, hidden internals*)
-    (string list * stamp) Symtab.table;                    (*externals*)
+    (string list * string list) Symtab.table *   (*internals, hidden internals*)
+    string list Symtab.table;                    (*externals*)
 
 val empty = NameSpace (Symtab.empty, Symtab.empty);
 
 fun lookup (NameSpace (tab, _)) xname =
   (case Symtab.lookup tab xname of
     NONE => (xname, true)
-  | SOME (([], []), _) => (xname, true)
-  | SOME (([name], _), _) => (name, true)
-  | SOME ((name :: _, _), _) => (name, false)
-  | SOME (([], name' :: _), _) => (hidden name', true));
+  | SOME ([], []) => (xname, true)
+  | SOME ([name], _) => (name, true)
+  | SOME (name :: _, _) => (name, false)
+  | SOME ([], name' :: _) => (hidden name', true));
 
-fun get_accesses (NameSpace (_, tab)) name =
-  (case Symtab.lookup tab name of
+fun get_accesses (NameSpace (_, xtab)) name =
+  (case Symtab.lookup xtab name of
     NONE => [name]
-  | SOME (xnames, _) => xnames);
+  | SOME xnames => xnames);
 
 fun put_accesses name xnames (NameSpace (tab, xtab)) =
-  NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
+  NameSpace (tab, Symtab.update (name, xnames) xtab);
 
-fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, ((names, _), _)) =>
+fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, (names, _)) =>
   if not (null names) andalso hd names = name then cons xname else I) tab [];
 
 
@@ -183,8 +181,7 @@
 local
 
 fun map_space f xname (NameSpace (tab, xtab)) =
-  NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
-    (fn (entry, _) => (f entry, stamp ())) tab, xtab);
+  NameSpace (Symtab.map_default (xname, ([], [])) f tab, xtab);
 
 in
 
@@ -217,15 +214,13 @@
 fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
   let
     val tab' = (tab1, tab2) |> Symtab.join
-      (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
-        if stamp1 = stamp2 then raise Symtab.SAME
-        else
-          ((Library.merge (op =) (names1, names2),
-            Library.merge (op =) (names1', names2')), stamp ())));
+      (K (fn names as ((names1, names1'), (names2, names2')) =>
+        if pointer_eq names then raise Symtab.SAME
+        else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
     val xtab' = (xtab1, xtab2) |> Symtab.join
-      (K (fn ((xnames1, stamp1), (xnames2, stamp2)) =>
-        if stamp1 = stamp2 then raise Symtab.SAME
-        else (Library.merge (op =) (xnames1, xnames2), stamp ())));
+      (K (fn xnames =>
+        if pointer_eq xnames then raise Symtab.SAME
+        else (Library.merge (op =) xnames)));
   in NameSpace (tab', xtab') end;
 
 
@@ -277,32 +272,33 @@
   in fold mk_prefix end;
 
 
-(* declarations *)
+(* full name *)
+
+fun full (Naming (path, (qualify, _))) = qualify path;
 
-fun full_internal (Naming (path, (qualify, _))) = qualify path;
+fun full_name naming binding =
+  let
+    val (prefix, qualifier, bname) = Binding.dest binding;
+    val naming' = apply_prefix (prefix @ qualifier) naming;
+  in full naming' bname end;
+
+
+(* declaration *)
 
-fun declare_internal naming name space =
-  if is_hidden name then
-    error ("Attempt to declare hidden name " ^ quote name)
-  else
-    let
-      val names = explode_name name;
-      val _ = (null names orelse exists (fn s => s = "") names
-          orelse exists_string (fn s => s = "\"") name) andalso
-        error ("Bad name declaration " ^ quote name);
-      val (accs, accs') = pairself (map implode_name) (accesses naming names);
-    in space |> fold (add_name name) accs |> put_accesses name accs' end;
+fun declare naming binding space =
+  let
+    val (prefix, qualifier, bname) = Binding.dest binding;
+    val naming' = apply_prefix (prefix @ qualifier) naming;
+    val name = full naming' bname;
+    val names = explode_name name;
 
-fun full_name naming b =
-  let val (prefix, qualifier, bname) = Binding.dest b
-  in full_internal (apply_prefix (prefix @ qualifier) naming) bname end;
+    val _ = (null names orelse exists (fn s => s = "" orelse s = "??") names
+        orelse exists_string (fn s => s = "\"") name) andalso
+      error ("Bad name declaration " ^ quote (Binding.str_of binding));
 
-fun declare bnaming b =
-  let
-    val (prefix, qualifier, bname) = Binding.dest b;
-    val naming = apply_prefix (prefix @ qualifier) bnaming;
-    val name = full_internal naming bname;
-  in declare_internal naming name #> pair name end;
+    val (accs, accs') = pairself (map implode_name) (accesses naming' names);
+    val space' = space |> fold (add_name name) accs |> put_accesses name accs';
+  in (name, space') end;
 
 
 
@@ -310,12 +306,11 @@
 
 type 'a table = T * 'a Symtab.table;
 
-val empty_table = (empty, Symtab.empty);
+fun bind naming (binding, x) (space, tab) =
+  let val (name, space') = declare naming binding space
+  in (name, (space', Symtab.update_new (name, x) tab)) end;
 
-fun bind naming (b, x) (space, tab) =
-  let
-    val (name, space') = declare naming b space;
-  in (name, (space', Symtab.update_new (name, x) tab)) end;
+val empty_table = (empty, Symtab.empty);
 
 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   (merge (space1, space2), Symtab.merge eq (tab1, tab2));