# HG changeset patch
# User wenzelm
# Date 1256421957 -7200
# Node ID 9d7d0bef2a777ddffbfe7c1e55387cee88fd81a2
# Parent  9d501e11084a72f9f9174b8cd0d54e5926f46ffa# Parent  e3463e6db704b5d18c072d48595cfe2dda72e67a
merged

diff -r e3463e6db704 -r 9d7d0bef2a77 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/HOL/Product_Type.thy	Sun Oct 25 00:05:57 2009 +0200
@@ -6,7 +6,7 @@
 header {* Cartesian products *}
 
 theory Product_Type
-imports Inductive
+imports Inductive Nat
 uses
   ("Tools/split_rule.ML")
   ("Tools/inductive_set.ML")
diff -r e3463e6db704 -r 9d7d0bef2a77 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -144,7 +144,7 @@
     val (tab, monos) = get_inductives ctxt;
     val space = Consts.space_of (ProofContext.consts_of ctxt);
   in
-    [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
+    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))),
      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
     |> Pretty.chunks |> Pretty.writeln
   end;
diff -r e3463e6db704 -r 9d7d0bef2a77 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -317,7 +317,7 @@
       |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
       |> fold meet_random insts;
   in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
-  end handle CLASS_ERROR => NONE;
+  end handle Sorts.CLASS_ERROR _ => NONE;
 
 fun ensure_random_datatype config raw_tycos thy =
   let
diff -r e3463e6db704 -r 9d7d0bef2a77 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/HOL/Tools/record.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -1810,7 +1810,7 @@
 
 fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
   let
-    val external_names = NameSpace.external_names (Sign.naming_of thy);
+    val external_names = Name_Space.external_names (Sign.naming_of thy);
 
     val alphas = map fst args;
     val name = Sign.full_bname thy bname;
diff -r e3463e6db704 -r 9d7d0bef2a77 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -355,7 +355,7 @@
     if run_blacklist_filter andalso is_package_def name then I
     else
       let val xname = Facts.extern facts name in
-        if NameSpace.is_hidden xname then I
+        if Name_Space.is_hidden xname then I
         else cons (xname, filter_out ResAxioms.bad_for_atp ths)
       end) facts [];
 
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/General/markup.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -18,6 +18,9 @@
   val kindN: string
   val internalK: string
   val property_internal: Properties.property
+  val entityN: string val entity: string -> T
+  val defN: string
+  val refN: string
   val lineN: string
   val columnN: string
   val offsetN: string
@@ -161,6 +164,14 @@
 val property_internal = (kindN, internalK);
 
 
+(* formal entities *)
+
+val (entityN, entity) = markup_string "entity" nameN;
+
+val defN = "def";
+val refN = "ref";
+
+
 (* position *)
 
 val lineN = "line";
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/General/markup.scala	Sun Oct 25 00:05:57 2009 +0200
@@ -15,6 +15,13 @@
   val KIND = "kind"
 
 
+  /* formal entities */
+
+  val ENTITY = "entity"
+  val DEF = "def"
+  val REF = "ref"
+
+
   /* position */
 
   val LINE = "line"
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/General/name_space.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -20,7 +20,9 @@
   val hidden: string -> string
   val is_hidden: string -> bool
   type T
-  val empty: T
+  val empty: string -> T
+  val kind_of: T -> string
+  val the_entry: T -> string -> {is_system: bool, pos: Position.T, id: serial}
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
@@ -29,7 +31,7 @@
   val merge: T * T -> T
   type naming
   val default_naming: naming
-  val declare: naming -> binding -> T -> string * T
+  val declare: bool -> naming -> binding -> T -> string * T
   val full_name: naming -> binding -> string
   val external_names: naming -> string -> string list
   val add_path: string -> naming -> naming
@@ -37,16 +39,16 @@
   val parent_path: naming -> naming
   val mandatory_path: string -> naming -> naming
   type 'a table = T * 'a Symtab.table
-  val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
-  val empty_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 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*) ->
+    'a table * 'a table -> 'a table
   val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
 end;
 
-structure NameSpace: NAME_SPACE =
+structure Name_Space: NAME_SPACE =
 struct
 
 
@@ -58,33 +60,71 @@
 val is_hidden = String.isPrefix "??.";
 
 
+(* datatype entry *)
+
+type entry =
+ {externals: xstring list,
+  is_system: bool,
+  pos: Position.T,
+  id: serial};
+
+fun str_of_entry def (name, {pos, id, ...}: entry) =
+  let
+    val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id);
+    val props = occurrence :: Position.properties_of pos;
+  in Markup.markup (Markup.properties props (Markup.entity name)) name end;
+
+fun err_dup kind entry1 entry2 =
+  error ("Duplicate " ^ kind ^ " declaration " ^
+    quote (str_of_entry true entry1) ^ " vs. " ^ quote (str_of_entry true entry2));
+
+
 (* datatype T *)
 
 datatype T =
-  NameSpace of
-    (string list * string list) Symtab.table *   (*internals, hidden internals*)
-    xstring list Symtab.table;                   (*externals*)
+  Name_Space of
+   {kind: string,
+    internals: (string list * string list) Symtab.table,  (*visible, hidden*)
+    entries: entry Symtab.table};
+
+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}) =
+  make_name_space (f (kind, internals, entries));
+
+fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
+  (kind, Symtab.map_default (xname, ([], [])) f internals, entries));
+
 
-val empty = NameSpace (Symtab.empty, Symtab.empty);
+fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);
+
+fun kind_of (Name_Space {kind, ...}) = kind;
 
-fun lookup (NameSpace (tab, _)) xname =
-  (case Symtab.lookup tab xname of
+fun the_entry (Name_Space {kind, entries, ...}) name =
+  (case Symtab.lookup entries name of
+    NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
+  | SOME {is_system, pos, id, ...} => {is_system = is_system, pos = pos, id = id});
+
+
+(* name accesses *)
+
+fun lookup (Name_Space {internals, ...}) xname =
+  (case Symtab.lookup internals xname of
     NONE => (xname, true)
   | SOME ([], []) => (xname, true)
   | SOME ([name], _) => (name, true)
   | SOME (name :: _, _) => (name, false)
   | SOME ([], name' :: _) => (hidden name', true));
 
-fun get_accesses (NameSpace (_, xtab)) name =
-  (case Symtab.lookup xtab name of
+fun get_accesses (Name_Space {entries, ...}) name =
+  (case Symtab.lookup entries name of
     NONE => [name]
-  | SOME xnames => xnames);
+  | SOME {externals, ...} => externals);
 
-fun put_accesses name xnames (NameSpace (tab, xtab)) =
-  NameSpace (tab, Symtab.update (name, xnames) xtab);
-
-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 [];
+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 [];
 
 
 (* intern and extern *)
@@ -116,21 +156,13 @@
     unique_names = ! unique_names} space name;
 
 
-(* basic operations *)
-
-local
-
-fun map_space f xname (NameSpace (tab, xtab)) =
-  NameSpace (Symtab.map_default (xname, ([], [])) f tab, xtab);
+(* modify internals *)
 
-in
-
-val del_name = map_space o apfst o remove (op =);
-fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
-val add_name = map_space o apfst o update (op =);
-val add_name' = map_space o apsnd o update (op =);
-
-end;
+val del_name = map_internals o apfst o remove (op =);
+fun del_name_extra name =
+  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
+val add_name = map_internals o apfst o update (op =);
+val add_name' = map_internals o apsnd o update (op =);
 
 
 (* hide *)
@@ -152,17 +184,24 @@
 
 (* merge *)
 
-fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
+fun merge
+  (Name_Space {kind = kind1, internals = internals1, entries = entries1},
+    Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
   let
-    val tab' = (tab1, tab2) |> Symtab.join
+    val kind' =
+      if kind1 = kind2 then kind1
+      else error ("Attempt to merge different kinds of name spaces " ^
+        quote kind1 ^ " vs. " ^ quote kind2);
+    val internals' = (internals1, internals2) |> Symtab.join
       (K (fn ((names1, names1'), (names2, names2')) =>
-        if pointer_eq (names1, names2) andalso pointer_eq (names1', names2') then raise Symtab.SAME
+        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 xtab' = (xtab1, xtab2) |> Symtab.join
-      (K (fn xnames =>
-        if pointer_eq xnames then raise Symtab.SAME
-        else (Library.merge (op =) xnames)));
-  in NameSpace (tab', xtab') end;
+    val entries' = (entries1, entries2) |> Symtab.join
+      (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;
 
 
 
@@ -225,13 +264,27 @@
 
 (* declaration *)
 
-fun declare naming binding space =
+fun new_entry strict entry =
+  map_name_space (fn (kind, internals, entries) =>
+    let
+      val entries' =
+        (if strict then Symtab.update_new else Symtab.update) entry entries
+          handle Symtab.DUP dup =>
+            err_dup kind (dup, the (Symtab.lookup entries dup)) entry;
+    in (kind, internals, entries') end);
+
+fun declare strict naming binding space =
   let
     val names = full naming binding;
     val name = Long_Name.implode names;
     val _ = name = "" andalso err_bad binding;
     val (accs, accs') = accesses naming binding;
-    val space' = space |> fold (add_name name) accs |> put_accesses name accs';
+    val entry =
+     {externals = accs',
+      is_system = false,
+      pos = Position.default (Binding.pos_of binding),
+      id = serial ()};
+    val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
   in (name, space') end;
 
 
@@ -240,14 +293,14 @@
 
 type 'a table = T * 'a Symtab.table;
 
-fun define naming (binding, x) (space, tab) =
-  let val (name, space') = declare naming binding space
-  in (name, (space', Symtab.update_new (name, x) tab)) end;
+fun define strict naming (binding, x) (space, tab) =
+  let val (name, space') = declare strict naming binding space
+  in (name, (space', Symtab.update (name, x) tab)) end;
 
-val empty_table = (empty, Symtab.empty);
+fun empty_table kind = (empty kind, Symtab.empty);
 
-fun merge_tables eq ((space1, tab1), (space2, tab2)) =
-  (merge (space1, space2), Symtab.merge eq (tab1, tab2));
+fun merge_tables ((space1, tab1), (space2, tab2)) =
+  (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
 
 fun join_tables f ((space1, tab1), (space2, tab2)) =
   (merge (space1, space2), Symtab.join f (tab1, tab2));
@@ -261,6 +314,6 @@
 
 end;
 
-structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
+structure Basic_Name_Space: BASIC_NAME_SPACE = Name_Space;
 open Basic_Name_Space;
 
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/General/position.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -37,6 +37,7 @@
   val range: T -> T -> range
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
+  val default: T -> T
 end;
 
 structure Position: POSITION =
@@ -178,4 +179,8 @@
 
 end;
 
+fun default pos =
+  if pos = none then thread_data ()
+  else pos;
+
 end;
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -67,35 +67,33 @@
 
 structure Attributes = TheoryDataFun
 (
-  type T = (((src -> attribute) * string) * stamp) NameSpace.table;
-  val empty = NameSpace.empty_table;
+  type T = ((src -> attribute) * string) Name_Space.table;
+  val empty = Name_Space.empty_table "attribute";
   val copy = I;
   val extend = I;
-  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
-    error ("Attempt to merge different versions of attribute " ^ quote dup);
+  fun merge _ tables : T = Name_Space.merge_tables tables;
 );
 
 fun print_attributes thy =
   let
     val attribs = Attributes.get thy;
-    fun prt_attr (name, ((_, comment), _)) = Pretty.block
+    fun prt_attr (name, (_, comment)) = Pretty.block
       [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   in
-    [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
+    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table attribs))]
     |> Pretty.chunks |> Pretty.writeln
   end;
 
-fun add_attribute name att comment thy = thy |> Attributes.map (fn atts =>
-  #2 (NameSpace.define (Sign.naming_of thy) (name, ((att, comment), stamp ())) atts)
-    handle Symtab.DUP dup => error ("Duplicate declaration of attribute " ^ quote dup));
+fun add_attribute name att comment thy = thy
+  |> Attributes.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (att, comment)));
 
 
 (* name space *)
 
-val intern = NameSpace.intern o #1 o Attributes.get;
+val intern = Name_Space.intern o #1 o Attributes.get;
 val intern_src = Args.map_name o intern;
 
-val extern = NameSpace.extern o #1 o Attributes.get o ProofContext.theory_of;
+val extern = Name_Space.extern o #1 o Attributes.get o ProofContext.theory_of;
 
 
 (* pretty printing *)
@@ -117,7 +115,7 @@
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup attrs name of
           NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
-        | SOME ((att, _), _) => (Position.report (Markup.attribute name) pos; att src))
+        | SOME (att, _) => (Position.report (Markup.attribute name) pos; att src))
       end;
   in attr end;
 
@@ -340,7 +338,7 @@
         Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
           Pretty.str (Config.print_value value)]
       end;
-    val configs = NameSpace.extern_table (#1 (Attributes.get thy), Configs.get thy);
+    val configs = Name_Space.extern_table (#1 (Attributes.get thy), Configs.get thy);
   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
 
 
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -400,7 +400,7 @@
     val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
     val {classes, ...} = Sorts.rep_algebra algebra;
     fun entry (c, (i, (_, cs))) =
-      (i, {name = NameSpace.extern space c, ID = c, parents = cs,
+      (i, {name = Name_Space.extern space c, ID = c, parents = cs,
             dir = "", unfold = true, path = ""});
     val gr =
       Graph.fold (cons o entry) classes []
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -17,7 +17,7 @@
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val checkpoint: local_theory -> local_theory
-  val full_naming: local_theory -> NameSpace.naming
+  val full_naming: local_theory -> Name_Space.naming
   val full_name: local_theory -> binding -> string
   val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val theory: (theory -> theory) -> local_theory -> local_theory
@@ -139,9 +139,9 @@
 
 fun full_naming lthy =
   Sign.naming_of (ProofContext.theory_of lthy)
-  |> NameSpace.mandatory_path (#theory_prefix (get_lthy lthy));
+  |> Name_Space.mandatory_path (#theory_prefix (get_lthy lthy));
 
-fun full_name naming = NameSpace.full_name (full_naming naming);
+fun full_name naming = Name_Space.full_name (full_naming naming);
 
 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
   |> Sign.mandatory_path (#theory_prefix (get_lthy lthy))
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -124,15 +124,15 @@
 
 structure Locales = TheoryDataFun
 (
-  type T = locale NameSpace.table;
-  val empty = NameSpace.empty_table;
+  type T = locale Name_Space.table;
+  val empty = Name_Space.empty_table "locale";
   val copy = I;
   val extend = I;
-  fun merge _ = NameSpace.join_tables (K merge_locale);
+  fun merge _ = Name_Space.join_tables (K merge_locale);
 );
 
-val intern = NameSpace.intern o #1 o Locales.get;
-val extern = NameSpace.extern o #1 o Locales.get;
+val intern = Name_Space.intern o #1 o Locales.get;
+val extern = Name_Space.extern o #1 o Locales.get;
 
 val get_locale = Symtab.lookup o #2 o Locales.get;
 val defined = Symtab.defined o #2 o Locales.get;
@@ -143,7 +143,7 @@
   | NONE => error ("Unknown locale " ^ quote name));
 
 fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
-  thy |> Locales.map (NameSpace.define (Sign.naming_of thy)
+  thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
     (binding,
       mk_locale ((parameters, spec, intros, axioms),
         ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
@@ -153,7 +153,7 @@
   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
 
 fun print_locales thy =
-  Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (Locales.get thy)))
+  Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
   |> Pretty.writeln;
 
 
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/Isar/method.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -322,32 +322,30 @@
 
 structure Methods = TheoryDataFun
 (
-  type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
-  val empty = NameSpace.empty_table;
+  type T = ((src -> Proof.context -> method) * string) Name_Space.table;
+  val empty = Name_Space.empty_table "method";
   val copy = I;
   val extend = I;
-  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
-    error ("Attempt to merge different versions of method " ^ quote dup);
+  fun merge _ tables : T = Name_Space.merge_tables tables;
 );
 
 fun print_methods thy =
   let
     val meths = Methods.get thy;
-    fun prt_meth (name, ((_, comment), _)) = Pretty.block
+    fun prt_meth (name, (_, comment)) = Pretty.block
       [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   in
-    [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
+    [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table meths))]
     |> Pretty.chunks |> Pretty.writeln
   end;
 
-fun add_method name meth comment thy = thy |> Methods.map (fn meths =>
-  #2 (NameSpace.define (Sign.naming_of thy) (name, ((meth, comment), stamp ())) meths)
-    handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup));
+fun add_method name meth comment thy = thy
+  |> Methods.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (meth, comment)));
 
 
 (* get methods *)
 
-val intern = NameSpace.intern o #1 o Methods.get;
+val intern = Name_Space.intern o #1 o Methods.get;
 val defined = Symtab.defined o #2 o Methods.get;
 
 fun method_i thy =
@@ -357,11 +355,11 @@
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup meths name of
           NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
-        | SOME ((mth, _), _) => (Position.report (Markup.method name) pos; mth src))
+        | SOME (mth, _) => (Position.report (Markup.method name) pos; mth src))
       end;
   in meth end;
 
-fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy)));
+fun method thy = method_i thy o Args.map_name (Name_Space.intern (#1 (Methods.get thy)));
 
 
 (* method setup *)
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/Isar/object_logic.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -90,7 +90,7 @@
     val base_sort = get_base_sort thy;
     val b = Binding.map_name (Syntax.type_name mx) a;
     val _ = has_duplicates (op =) vs andalso
-      error ("Duplicate parameters in type declaration: " ^ quote (Binding.str_of b));
+      error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
     val name = Sign.full_name thy b;
     val n = length vs;
     val T = Type (name, map (fn v => TFree (v, [])) vs);
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -21,7 +21,7 @@
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val abbrev_mode: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
-  val naming_of: Proof.context -> NameSpace.naming
+  val naming_of: Proof.context -> Name_Space.naming
   val full_name: Proof.context -> binding -> string
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
@@ -170,7 +170,7 @@
 datatype ctxt =
   Ctxt of
    {mode: mode,                                       (*inner syntax mode*)
-    naming: NameSpace.naming,                         (*local naming conventions*)
+    naming: Name_Space.naming,                        (*local naming conventions*)
     syntax: LocalSyntax.T,                            (*local syntax*)
     consts: Consts.T * Consts.T,                      (*local/global consts*)
     facts: Facts.T,                                   (*local facts*)
@@ -180,7 +180,7 @@
   Ctxt {mode = mode, naming = naming, syntax = syntax,
     consts = consts, facts = facts, cases = cases};
 
-val local_naming = NameSpace.default_naming |> NameSpace.add_path "local";
+val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
 
 structure ContextData = ProofDataFun
 (
@@ -231,7 +231,7 @@
   map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
 
 val naming_of = #naming o rep_context;
-val full_name = NameSpace.full_name o naming_of;
+val full_name = Name_Space.full_name o naming_of;
 
 val syntax_of = #syntax o rep_context;
 val syn_of = LocalSyntax.syn_of o syntax_of;
@@ -924,10 +924,10 @@
 
 (* name space operations *)
 
-val add_path        = map_naming o NameSpace.add_path;
-val mandatory_path  = map_naming o NameSpace.mandatory_path;
-val restore_naming  = map_naming o K o naming_of;
-val reset_naming    = map_naming (K local_naming);
+val add_path = map_naming o Name_Space.add_path;
+val mandatory_path = map_naming o Name_Space.mandatory_path;
+val restore_naming = map_naming o K o naming_of;
+val reset_naming = map_naming (K local_naming);
 
 
 (* facts *)
@@ -1230,7 +1230,7 @@
       | add_abbr (c, (T, SOME t)) =
           if not show_globals andalso Symtab.defined globals c then I
           else cons (c, Logic.mk_equals (Const (c, T), t));
-    val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));
+    val abbrevs = Name_Space.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));
   in
     if null abbrevs andalso not (! verbose) then []
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -420,9 +420,9 @@
   ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
   ("show_structs", setmp_CRITICAL show_structs o boolean),
   ("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
-  ("long_names", setmp_CRITICAL NameSpace.long_names o boolean),
-  ("short_names", setmp_CRITICAL NameSpace.short_names o boolean),
-  ("unique_names", setmp_CRITICAL NameSpace.unique_names o boolean),
+  ("long_names", setmp_CRITICAL Name_Space.long_names o boolean),
+  ("short_names", setmp_CRITICAL Name_Space.short_names o boolean),
+  ("unique_names", setmp_CRITICAL Name_Space.unique_names o boolean),
   ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
   ("display", setmp_CRITICAL display o boolean),
   ("break", setmp_CRITICAL break o boolean),
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -326,7 +326,7 @@
 local
 
 val index_ord = option_ord (K EQUAL);
-val hidden_ord = bool_ord o pairself NameSpace.is_hidden;
+val hidden_ord = bool_ord o pairself Name_Space.is_hidden;
 val qual_ord = int_ord o pairself (length o Long_Name.explode);
 val txt_ord = int_ord o pairself size;
 
@@ -355,7 +355,8 @@
     val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
 
     val shorten =
-      NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space;
+      Name_Space.extern_flags
+        {long_names = false, short_names = false, unique_names = false} space;
 
     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
           nicer_name (shorten x, i) (shorten y, j)
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/codegen.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -337,15 +337,16 @@
     val tc = Sign.intern_type thy s;
   in
     case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
-      SOME ((Type.LogicalType i, _), _) =>
+      SOME (Type.LogicalType i, _) =>
         if num_args_of (fst syn) > i then
           error ("More arguments than corresponding type constructor " ^ s)
-        else (case AList.lookup (op =) types tc of
-          NONE => CodegenData.put {codegens = codegens,
-            tycodegens = tycodegens, consts = consts,
-            types = (tc, syn) :: types,
-            preprocs = preprocs, modules = modules} thy
-        | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
+        else
+          (case AList.lookup (op =) types tc of
+            NONE => CodegenData.put {codegens = codegens,
+              tycodegens = tycodegens, consts = consts,
+              types = (tc, syn) :: types,
+              preprocs = preprocs, modules = modules} thy
+          | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
     | _ => error ("Not a type constructor: " ^ s)
   end;
 
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/consts.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -11,15 +11,15 @@
   val eq_consts: T * T -> bool
   val retrieve_abbrevs: T -> string list -> term -> (term * term) list
   val dest: T ->
-   {constants: (typ * term option) NameSpace.table,
-    constraints: typ NameSpace.table}
+   {constants: (typ * term option) Name_Space.table,
+    constraints: typ Name_Space.table}
   val the_type: T -> string -> typ                             (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   val type_scheme: T -> string -> typ                          (*exception TYPE*)
   val the_tags: T -> string -> Properties.T                    (*exception TYPE*)
   val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   val the_constraint: T -> string -> typ                       (*exception TYPE*)
-  val space_of: T -> NameSpace.T
+  val space_of: T -> Name_Space.T
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val extern_early: T -> string -> xstring
@@ -29,9 +29,9 @@
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T
+  val declare: bool -> Name_Space.naming -> Properties.T -> binding * typ -> T -> T
   val constrain: string * typ option -> T -> T
-  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
+  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> Properties.T ->
     binding * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
@@ -50,7 +50,7 @@
 type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
 
 datatype T = Consts of
- {decls: ((decl * abbrev option) * serial) NameSpace.table,
+ {decls: (decl * abbrev option) Name_Space.table,
   constraints: typ Symtab.table,
   rev_abbrevs: (term * term) Item_Net.T Symtab.table};
 
@@ -84,7 +84,7 @@
 
 fun dest (Consts {decls = (space, decls), constraints, ...}) =
  {constants = (space,
-    Symtab.fold (fn (c, (({T, ...}, abbr), _)) =>
+    Symtab.fold (fn (c, ({T, ...}, abbr)) =>
       Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty),
   constraints = (space, constraints)};
 
@@ -93,7 +93,7 @@
 
 fun the_const (Consts {decls = (_, tab), ...}) c =
   (case Symtab.lookup tab c of
-    SOME (decl, _) => decl
+    SOME decl => decl
   | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
 
 fun the_type consts c =
@@ -123,8 +123,8 @@
 
 fun space_of (Consts {decls = (space, _), ...}) = space;
 
-val intern = NameSpace.intern o space_of;
-val extern = NameSpace.extern o space_of;
+val intern = Name_Space.intern o space_of;
+val extern = Name_Space.extern o space_of;
 
 fun extern_early consts c =
   (case try (the_const consts) c of
@@ -221,27 +221,20 @@
 
 (** build consts **)
 
-fun err_dup_const c =
-  error ("Duplicate declaration of constant " ^ quote c);
-
-fun extend_decls naming decl tab = NameSpace.define naming decl tab
-  handle Symtab.DUP c => err_dup_const c;
-
-
 (* name space *)
 
 fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) =>
-  (apfst (NameSpace.hide fully c) decls, constraints, rev_abbrevs));
+  (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs));
 
 
 (* declarations *)
 
-fun declare authentic naming tags (b, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
-  let
-    val tags' = tags |> Position.default_properties (Position.thread_data ());
-    val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
-    val (_, decls') = decls |> extend_decls naming (b, ((decl, NONE), serial ()));
-  in (decls', constraints, rev_abbrevs) end);
+fun declare authentic naming tags (b, declT) =
+  map_consts (fn (decls, constraints, rev_abbrevs) =>
+    let
+      val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic};
+      val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
+    in (decls', constraints, rev_abbrevs) end);
 
 
 (* constraints *)
@@ -278,7 +271,7 @@
     val force_expand = mode = PrintMode.internal;
 
     val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
-      error ("Illegal schematic variables on rhs of abbreviation: " ^ Binding.str_of b);
+      error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
 
     val rhs = raw_rhs
       |> Term.map_types (Type.cert_typ tsig)
@@ -286,15 +279,14 @@
       |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;
     val T = Term.fastype_of rhs;
-    val lhs = Const (NameSpace.full_name naming b, T);
+    val lhs = Const (Name_Space.full_name naming b, T);
   in
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
-        val tags' = tags |> Position.default_properties (Position.thread_data ());
-        val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
+        val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
         val (_, decls') = decls
-          |> extend_decls naming (b, ((decl, SOME abbr), serial ()));
+          |> Name_Space.define true naming (b, (decl, SOME abbr));
         val rev_abbrevs' = rev_abbrevs
           |> insert_abbrevs mode (rev_abbrev lhs rhs);
       in (decls', constraints, rev_abbrevs') end)
@@ -313,14 +305,13 @@
 
 (* empty and merge *)
 
-val empty = make_consts (NameSpace.empty_table, Symtab.empty, Symtab.empty);
+val empty = make_consts (Name_Space.empty_table "constant", Symtab.empty, Symtab.empty);
 
 fun merge
    (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
     Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
   let
-    val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
-      handle Symtab.DUP c => err_dup_const c;
+    val decls' = Name_Space.merge_tables (decls1, decls2);
     val constraints' = Symtab.join (K fst) (constraints1, constraints2);
     val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
   in make_consts (decls', constraints', rev_abbrevs') end;
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/display.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -146,14 +146,14 @@
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
 
     val tfrees = map (fn v => TFree (v, []));
-    fun pretty_type syn (t, ((Type.LogicalType n, _), _)) =
+    fun pretty_type syn (t, (Type.LogicalType n, _)) =
           if syn then NONE
           else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
-      | pretty_type syn (t, ((Type.Abbreviation (vs, U, syn'), _), _)) =
+      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
           if syn <> syn' then NONE
           else SOME (Pretty.block
             [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
-      | pretty_type syn (t, ((Type.Nonterminal, _), _)) =
+      | pretty_type syn (t, (Type.Nonterminal, _)) =
           if not syn then NONE
           else SOME (prt_typ (Type (t, [])));
 
@@ -179,25 +179,25 @@
     val {restricts, reducts} = Defs.dest defs;
     val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
     val {constants, constraints} = Consts.dest consts;
-    val extern_const = NameSpace.extern (#1 constants);
+    val extern_const = Name_Space.extern (#1 constants);
     val {classes, default, types, ...} = Type.rep_tsig tsig;
     val (class_space, class_algebra) = classes;
     val {classes, arities} = Sorts.rep_algebra class_algebra;
 
-    val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
-    val tdecls = NameSpace.dest_table types;
-    val arties = NameSpace.dest_table (Sign.type_space thy, arities);
+    val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
+    val tdecls = Name_Space.dest_table types;
+    val arties = Name_Space.dest_table (Sign.type_space thy, arities);
 
     fun prune_const c = not verbose andalso
       member (op =) (Consts.the_tags consts c) Markup.property_internal;
-    val cnsts = NameSpace.extern_table (#1 constants,
+    val cnsts = Name_Space.extern_table (#1 constants,
       Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
 
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
-    val cnstrs = NameSpace.extern_table constraints;
+    val cnstrs = Name_Space.extern_table constraints;
 
-    val axms = NameSpace.extern_table axioms;
+    val axms = Name_Space.extern_table axioms;
 
     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/drule.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -452,7 +452,7 @@
 
 val read_prop = certify o SimpleSyntax.read_prop;
 
-fun get_def thy = Thm.axiom thy o NameSpace.intern (Theory.axiom_space thy) o Thm.def_name;
+fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
 
 fun store_thm name th =
   Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/facts.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -20,7 +20,7 @@
   val selections: string * thm list -> (ref * thm) list
   type T
   val empty: T
-  val space_of: T -> NameSpace.T
+  val space_of: T -> Name_Space.T
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
@@ -31,9 +31,9 @@
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
-  val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
-  val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
-  val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
+  val add_global: Name_Space.naming -> binding * thm list -> T -> string * T
+  val add_local: bool -> Name_Space.naming -> binding * thm list -> T -> string * T
+  val add_dynamic: Name_Space.naming -> binding * (Context.generic -> thm list) -> T -> string * T
   val del: string -> T -> T
   val hide: bool -> string -> T -> T
 end;
@@ -122,11 +122,11 @@
 datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
 
 datatype T = Facts of
- {facts: (fact * serial) NameSpace.table,
+ {facts: fact Name_Space.table,
   props: thm Net.net};
 
 fun make_facts facts props = Facts {facts = facts, props = props};
-val empty = make_facts NameSpace.empty_table Net.empty;
+val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
 
 
 (* named facts *)
@@ -136,18 +136,19 @@
 val space_of = #1 o facts_of;
 val table_of = #2 o facts_of;
 
-val intern = NameSpace.intern o space_of;
-val extern = NameSpace.extern o space_of;
+val intern = Name_Space.intern o space_of;
+val extern = Name_Space.extern o space_of;
 
 val defined = Symtab.defined o table_of;
 
 fun lookup context facts name =
   (case Symtab.lookup (table_of facts) name of
     NONE => NONE
-  | SOME (Static ths, _) => SOME (true, ths)
-  | SOME (Dynamic f, _) => SOME (false, f context));
+  | SOME (Static ths) => SOME (true, ths)
+  | SOME (Dynamic f) => SOME (false, f context));
 
-fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;
+fun fold_static f =
+  Symtab.fold (fn (name, Static ths) => f (name, ths) | _ => I) o table_of;
 
 
 (* content difference *)
@@ -174,61 +175,52 @@
 
 (* merge facts *)
 
-fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
-
-(* FIXME stamp identity! *)
-fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2))
-  | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2;
-
 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   let
-    val facts' = NameSpace.merge_tables eq_entry (facts1, facts2)
-      handle Symtab.DUP dup => err_dup_fact dup;
+    val facts' = Name_Space.merge_tables (facts1, facts2);
     val props' = Net.merge (is_equal o prop_ord) (props1, props2);
   in make_facts facts' props' end;
 
 
 (* add static entries *)
 
-fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
+local
+
+fun add strict do_props naming (b, ths) (Facts {facts, props}) =
   let
-    val (name, facts') = if Binding.is_empty b then ("", facts)
-      else let
-        val (space, tab) = facts;
-        val (name, space') = NameSpace.declare naming b space;
-        val entry = (name, (Static ths, serial ()));
-        val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
-          handle Symtab.DUP dup => err_dup_fact dup;
-      in (name, (space', tab')) end;
+    val (name, facts') =
+      if Binding.is_empty b then ("", facts)
+      else Name_Space.define strict naming (b, Static ths) facts;
     val props' =
-      if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
+      if do_props
+      then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
       else props;
   in (name, make_facts facts' props') end;
 
-val add_global = add false false;
-val add_local = add true;
+in
+
+val add_global = add true false;
+val add_local = add false;
+
+end;
 
 
 (* add dynamic entries *)
 
-fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
-  let
-    val (name, space') = NameSpace.declare naming b space;
-    val entry = (name, (Dynamic f, serial ()));
-    val tab' = Symtab.update_new entry tab
-      handle Symtab.DUP dup => err_dup_fact dup;
-  in (name, make_facts (space', tab') props) end;
+fun add_dynamic naming (b, f) (Facts {facts, props}) =
+  let val (name, facts') = Name_Space.define true naming (b, Dynamic f) facts;
+  in (name, make_facts facts' props) end;
 
 
 (* remove entries *)
 
 fun del name (Facts {facts = (space, tab), props}) =
   let
-    val space' = NameSpace.hide true name space handle ERROR _ => space;
+    val space' = Name_Space.hide true name space handle ERROR _ => space;  (* FIXME handle?? *)
     val tab' = Symtab.delete_safe name tab;
   in make_facts (space', tab') props end;
 
 fun hide fully name (Facts {facts = (space, tab), props}) =
-  make_facts (NameSpace.hide fully name space, tab) props;
+  make_facts (Name_Space.hide fully name space, tab) props;
 
 end;
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/name.ML
--- a/src/Pure/name.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/name.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -45,7 +45,7 @@
 
 (* checked binding *)
 
-val of_binding = Long_Name.base_name o NameSpace.full_name NameSpace.default_naming;
+val of_binding = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
 
 
 (* encoded bounds *)
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/pure_thy.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -146,7 +146,7 @@
   else
     let
       val naming = Sign.naming_of thy;
-      val name = NameSpace.full_name naming b;
+      val name = Name_Space.full_name naming b;
       val (thy', thms') =
         register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
       val thms'' = map (Thm.transfer thy') thms';
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/sign.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -8,11 +8,11 @@
 signature SIGN =
 sig
   val rep_sg: theory ->
-   {naming: NameSpace.naming,
+   {naming: Name_Space.naming,
     syn: Syntax.syntax,
     tsig: Type.tsig,
     consts: Consts.T}
-  val naming_of: theory -> NameSpace.naming
+  val naming_of: theory -> Name_Space.naming
   val full_name: theory -> binding -> string
   val full_name_path: theory -> string -> binding -> string
   val full_bname: theory -> bstring -> string
@@ -44,9 +44,9 @@
   val const_typargs: theory -> string * typ -> typ list
   val const_instance: theory -> string * typ list -> typ
   val mk_const: theory -> string * typ list -> term
-  val class_space: theory -> NameSpace.T
-  val type_space: theory -> NameSpace.T
-  val const_space: theory -> NameSpace.T
+  val class_space: theory -> Name_Space.T
+  val type_space: theory -> Name_Space.T
+  val const_space: theory -> Name_Space.T
   val intern_class: theory -> xstring -> string
   val extern_class: theory -> string -> xstring
   val intern_type: theory -> xstring -> string
@@ -137,7 +137,7 @@
 (** datatype sign **)
 
 datatype sign = Sign of
- {naming: NameSpace.naming,     (*common naming conventions*)
+ {naming: Name_Space.naming,    (*common naming conventions*)
   syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
   tsig: Type.tsig,              (*order-sorted signature of types*)
   consts: Consts.T};            (*polymorphic constants*)
@@ -150,17 +150,17 @@
   type T = sign;
   val copy = I;
   fun extend (Sign {syn, tsig, consts, ...}) =
-    make_sign (NameSpace.default_naming, syn, tsig, consts);
+    make_sign (Name_Space.default_naming, syn, tsig, consts);
 
   val empty =
-    make_sign (NameSpace.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
+    make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
 
   fun merge pp (sign1, sign2) =
     let
       val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
       val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
 
-      val naming = NameSpace.default_naming;
+      val naming = Name_Space.default_naming;
       val syn = Syntax.merge_syntaxes syn1 syn2;
       val tsig = Type.merge_tsigs pp (tsig1, tsig2);
       val consts = Consts.merge (consts1, consts2);
@@ -182,10 +182,10 @@
 
 val naming_of = #naming o rep_sg;
 
-val full_name = NameSpace.full_name o naming_of;
-fun full_name_path thy path = NameSpace.full_name (NameSpace.add_path path (naming_of thy));
+val full_name = Name_Space.full_name o naming_of;
+fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
 
-fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
+fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
 fun full_bname_path thy path = full_name_path thy path o Binding.name;
 
 
@@ -240,12 +240,12 @@
 val type_space = #1 o #types o Type.rep_tsig o tsig_of;
 val const_space = Consts.space_of o consts_of;
 
-val intern_class = NameSpace.intern o class_space;
-val extern_class = NameSpace.extern o class_space;
-val intern_type = NameSpace.intern o type_space;
-val extern_type = NameSpace.extern o type_space;
-val intern_const = NameSpace.intern o const_space;
-val extern_const = NameSpace.extern o const_space;
+val intern_class = Name_Space.intern o class_space;
+val extern_class = Name_Space.extern o class_space;
+val intern_type = Name_Space.intern o type_space;
+val extern_type = Name_Space.extern o type_space;
+val intern_const = Name_Space.intern o const_space;
+val extern_const = Name_Space.extern o const_space;
 
 val intern_sort = map o intern_class;
 val extern_sort = map o extern_class;
@@ -526,8 +526,7 @@
 fun declare_const tags ((b, T), mx) thy =
   let
     val pos = Binding.pos_of b;
-    val tags' = Position.default_properties pos tags;
-    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
+    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags [(b, T, mx)] thy;
     val _ = Position.report (Markup.const_decl c) pos;
   in (const, thy') end;
 
@@ -612,10 +611,10 @@
 
 (* naming *)
 
-val add_path = map_naming o NameSpace.add_path;
-val root_path = map_naming NameSpace.root_path;
-val parent_path = map_naming NameSpace.parent_path;
-val mandatory_path = map_naming o NameSpace.mandatory_path;
+val add_path = map_naming o Name_Space.add_path;
+val root_path = map_naming Name_Space.root_path;
+val parent_path = map_naming Name_Space.parent_path;
+val mandatory_path = map_naming o Name_Space.mandatory_path;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/simplifier.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -143,18 +143,14 @@
 
 (** named simprocs **)
 
-fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
-
-
 (* data *)
 
 structure Simprocs = GenericDataFun
 (
-  type T = simproc NameSpace.table;
-  val empty = NameSpace.empty_table;
+  type T = simproc Name_Space.table;
+  val empty = Name_Space.empty_table "simproc";
   val extend = I;
-  fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
-    handle Symtab.DUP dup => err_dup_simproc dup;
+  fun merge _ simprocs = Name_Space.merge_tables simprocs;
 );
 
 
@@ -163,7 +159,7 @@
 fun get_simproc context xname =
   let
     val (space, tab) = Simprocs.get context;
-    val name = NameSpace.intern space xname;
+    val name = Name_Space.intern space xname;
   in
     (case Symtab.lookup tab name of
       SOME proc => proc
@@ -201,9 +197,7 @@
         val b' = Morphism.binding phi b;
         val simproc' = morph_simproc phi simproc;
       in
-        Simprocs.map (fn simprocs =>
-          NameSpace.define naming (b', simproc') simprocs |> snd
-            handle Symtab.DUP dup => err_dup_simproc dup)
+        Simprocs.map (#2 o Name_Space.define true naming (b', simproc'))
         #> map_ss (fn ss => ss addsimprocs [simproc'])
       end)
   end;
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/theory.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -19,7 +19,7 @@
   val checkpoint: theory -> theory
   val copy: theory -> theory
   val requires: theory -> string -> string -> unit
-  val axiom_space: theory -> NameSpace.T
+  val axiom_space: theory -> Name_Space.T
   val axiom_table: theory -> term Symtab.table
   val axioms_of: theory -> (string * term) list
   val all_axioms_of: theory -> (string * term) list
@@ -80,29 +80,27 @@
   perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
 
 datatype thy = Thy of
- {axioms: term NameSpace.table,
+ {axioms: term Name_Space.table,
   defs: Defs.T,
   wrappers: wrapper list * wrapper list};
 
 fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
 
-fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
-
 structure ThyData = TheoryDataFun
 (
   type T = thy;
-  val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
+  val empty_axioms = Name_Space.empty_table "axiom";
+  val empty = make_thy (empty_axioms, Defs.empty, ([], []));
   val copy = I;
 
-  fun extend (Thy {axioms = _, defs, wrappers}) =
-    make_thy (NameSpace.empty_table, defs, wrappers);
+  fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
 
   fun merge pp (thy1, thy2) =
     let
       val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
       val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
-      val axioms' = NameSpace.empty_table;
+      val axioms' = empty_axioms;
       val defs' = Defs.merge pp (defs1, defs2);
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
@@ -166,7 +164,7 @@
 
 fun read_axm thy (b, str) =
   cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
-    cat_error msg ("The error(s) above occurred in axiom: " ^ quote (Binding.str_of b));
+    cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
 
 
 (* add_axioms(_i) *)
@@ -176,8 +174,7 @@
 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   let
     val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
-    val axioms' = fold (snd oo NameSpace.define (Sign.naming_of thy)) axms axioms
-      handle Symtab.DUP dup => err_dup_axm dup;
+    val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms;
   in axioms' end);
 
 in
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/thm.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -1724,25 +1724,21 @@
 
 (* authentic derivation names *)
 
-fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
-
 structure Oracles = TheoryDataFun
 (
-  type T = serial NameSpace.table;
-  val empty = NameSpace.empty_table;
+  type T = unit Name_Space.table;
+  val empty = Name_Space.empty_table "oracle";
   val copy = I;
   val extend = I;
-  fun merge _ oracles : T = NameSpace.merge_tables (op =) oracles
-    handle Symtab.DUP dup => err_dup_ora dup;
+  fun merge _ oracles : T = Name_Space.merge_tables oracles;
 );
 
-val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
+val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
 
 fun add_oracle (b, oracle) thy =
   let
     val naming = Sign.naming_of thy;
-    val (name, tab') = NameSpace.define naming (b, serial ()) (Oracles.get thy)
-      handle Symtab.DUP _ => err_dup_ora (Binding.str_of b);
+    val (name, tab') = Name_Space.define true naming (b, ()) (Oracles.get thy);
     val thy' = Oracles.put tab' thy;
   in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
 
diff -r e3463e6db704 -r 9d7d0bef2a77 src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Oct 25 00:00:53 2009 +0200
+++ b/src/Pure/type.ML	Sun Oct 25 00:05:57 2009 +0200
@@ -14,9 +14,9 @@
     Nonterminal
   type tsig
   val rep_tsig: tsig ->
-   {classes: NameSpace.T * Sorts.algebra,
+   {classes: Name_Space.T * Sorts.algebra,
     default: sort,
-    types: ((decl * Properties.T) * serial) NameSpace.table,
+    types: (decl * Properties.T) Name_Space.table,
     log_types: string list}
   val empty_tsig: tsig
   val defaultS: tsig -> sort
@@ -70,12 +70,12 @@
   val eq_type: tyenv -> typ * typ -> bool
 
   (*extend and merge type signatures*)
-  val add_class: Pretty.pp -> NameSpace.naming -> binding * class list -> tsig -> tsig
+  val add_class: Pretty.pp -> Name_Space.naming -> binding * class list -> tsig -> tsig
   val hide_class: bool -> string -> tsig -> tsig
   val set_defsort: sort -> tsig -> tsig
-  val add_type: NameSpace.naming -> Properties.T -> binding * int -> tsig -> tsig
-  val add_abbrev: NameSpace.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
-  val add_nonterminal: NameSpace.naming -> Properties.T -> binding -> tsig -> tsig
+  val add_type: Name_Space.naming -> Properties.T -> binding * int -> tsig -> tsig
+  val add_abbrev: Name_Space.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
+  val add_nonterminal: Name_Space.naming -> Properties.T -> binding -> tsig -> tsig
   val hide_type: bool -> string -> tsig -> tsig
   val add_arity: Pretty.pp -> arity -> tsig -> tsig
   val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
@@ -94,18 +94,14 @@
   Abbreviation of string list * typ * bool |
   Nonterminal;
 
-fun str_of_decl (LogicalType _) = "logical type constructor"
-  | str_of_decl (Abbreviation _) = "type abbreviation"
-  | str_of_decl Nonterminal = "syntactic type";
-
 
 (* type tsig *)
 
 datatype tsig =
   TSig of {
-    classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
+    classes: Name_Space.T * Sorts.algebra,  (*order-sorted algebra of type classes*)
     default: sort,                          (*default sort on input*)
-    types: ((decl * Properties.T) * serial) NameSpace.table, (*declared types*)
+    types: (decl * Properties.T) Name_Space.table,  (*declared types*)
     log_types: string list};                (*logical types sorted by number of arguments*)
 
 fun rep_tsig (TSig comps) = comps;
@@ -113,18 +109,18 @@
 fun make_tsig (classes, default, types, log_types) =
   TSig {classes = classes, default = default, types = types, log_types = log_types};
 
-fun build_tsig ((space, classes), default, types) =
+fun build_tsig (classes, default, types) =
   let
     val log_types =
-      Symtab.fold (fn (c, ((LogicalType n, _), _)) => cons (c, n) | _ => I) (snd types) []
-      |> Library.sort (Library.int_ord o pairself snd) |> map fst;
-  in make_tsig ((space, classes), default, types, log_types) end;
+      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
+      |> Library.sort (int_ord o pairself snd) |> map fst;
+  in make_tsig (classes, default, types, log_types) end;
 
 fun map_tsig f (TSig {classes, default, types, log_types = _}) =
   build_tsig (f (classes, default, types));
 
 val empty_tsig =
-  build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table);
+  build_tsig ((Name_Space.empty "class", Sorts.empty_algebra), [], Name_Space.empty_table "type");
 
 
 (* classes and sorts *)
@@ -167,7 +163,7 @@
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
 
-fun lookup_type (TSig {types, ...}) = Option.map fst o Symtab.lookup (snd types);
+fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
 
 fun the_tags tsig c =
   (case lookup_type tsig c of
@@ -515,12 +511,12 @@
     let
       val cs' = map (cert_class tsig) cs
         handle TYPE (msg, _, _) => error msg;
-      val (c', space') = space |> NameSpace.declare naming c;
+      val (c', space') = space |> Name_Space.declare true naming c;
       val classes' = classes |> Sorts.add_class pp (c', cs');
     in ((space', classes'), default, types) end);
 
 fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
-  ((NameSpace.hide fully c space, classes), default, types));
+  ((Name_Space.hide fully c space, classes), default, types));
 
 
 (* arities *)
@@ -530,7 +526,7 @@
     val _ =
       (case lookup_type tsig t of
         SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else ()
-      | SOME (decl, _) => error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t)
+      | SOME _ => error ("Logical type constructor expected: " ^ quote t)
       | NONE => error (undecl_type t));
     val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
       handle TYPE (msg, _, _) => error msg;
@@ -559,68 +555,49 @@
 
 local
 
-fun err_in_decls c decl decl' =
-  let val s = str_of_decl decl and s' = str_of_decl decl' in
-    if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
-    else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
-  end;
-
-fun new_decl naming tags (c, decl) (space, types) =
-  let
-    val tags' = tags |> Position.default_properties (Position.thread_data ());
-    val (c', space') = NameSpace.declare naming c space;
-    val types' =
-      (case Symtab.lookup types c' of
-        SOME ((decl', _), _) => err_in_decls c' decl decl'
-      | NONE => Symtab.update (c', ((decl, tags'), serial ())) types);
-  in (space', types') end;
-
-fun the_decl (_, types) = fst o fst o the o Symtab.lookup types;
+fun new_decl naming tags (c, decl) types =
+  #2 (Name_Space.define true naming (c, (decl, tags)) types);
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let
     val (space', tab') = f types;
-    val _ = NameSpace.intern space' "dummy" = "dummy" orelse
+    val _ = Name_Space.intern space' "dummy" = "dummy" orelse
       error "Illegal declaration of dummy type";
   in (classes, default, (space', tab')) end);
 
 fun syntactic types (Type (c, Ts)) =
-      (case Symtab.lookup types c of SOME ((Nonterminal, _), _) => true | _ => false)
+      (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
         orelse exists (syntactic types) Ts
   | syntactic _ _ = false;
 
 in
 
 fun add_type naming tags (c, n) =
-  if n < 0 then error ("Bad type constructor declaration: " ^ quote (Binding.str_of c))
+  if n < 0 then error ("Bad type constructor declaration " ^ quote (Binding.str_of c))
   else map_types (new_decl naming tags (c, LogicalType n));
 
 fun add_abbrev naming tags (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   let
     fun err msg =
-      cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote (Binding.str_of a));
+      cat_error msg ("The error(s) above occurred in type abbreviation " ^ quote (Binding.str_of a));
     val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
       handle TYPE (msg, _, _) => err msg;
-  in
-    (case duplicates (op =) vs of
-      [] => []
-    | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
-    (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
-      [] => []
-    | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
-    types |> new_decl naming tags (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
-  end);
+    val _ =
+      (case duplicates (op =) vs of
+        [] => []
+      | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
+    val _ =
+      (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
+        [] => []
+      | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
+  in types |> new_decl naming tags (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
 
 fun add_nonterminal naming tags = map_types o new_decl naming tags o rpair Nonterminal;
 
-fun merge_types (types1, types2) =
-  NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2)
-    handle Symtab.DUP d => err_in_decls d (the_decl types1 d) (the_decl types2 d);
-
 end;
 
 fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) =>
-  (classes, default, (NameSpace.hide fully c space, types)));
+  (classes, default, (Name_Space.hide fully c space, types)));
 
 
 (* merge type signatures *)
@@ -632,10 +609,10 @@
     val (TSig {classes = (space2, classes2), default = default2, types = types2,
       log_types = _}) = tsig2;
 
-    val space' = NameSpace.merge (space1, space2);
+    val space' = Name_Space.merge (space1, space2);
     val classes' = Sorts.merge_algebra pp (classes1, classes2);
     val default' = Sorts.inter_sort classes' (default1, default2);
-    val types' = merge_types (types1, types2);
+    val types' = Name_Space.merge_tables (types1, types2);
   in build_tsig ((space', classes'), default', types') end;
 
 end;