diff -r d010f61d3702 -r ef0d77b1e687 src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Oct 24 19:22:39 2009 +0200
+++ b/src/Pure/type.ML	Sat Oct 24 19:24:50 2009 +0200
@@ -16,7 +16,7 @@
   val rep_tsig: tsig ->
    {classes: NameSpace.T * Sorts.algebra,
     default: sort,
-    types: ((decl * Properties.T) * serial) NameSpace.table,
+    types: (decl * Properties.T) NameSpace.table,
     log_types: string list}
   val empty_tsig: tsig
   val defaultS: tsig -> sort
@@ -94,10 +94,6 @@
   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 *)
 
@@ -105,7 +101,7 @@
   TSig of {
     classes: NameSpace.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) NameSpace.table,  (*declared types*)
     log_types: string list};                (*logical types sorted by number of arguments*)
 
 fun rep_tsig (TSig comps) = comps;
@@ -113,12 +109,12 @@
 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));
@@ -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,7 +511,7 @@
     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 |> NameSpace.declare true naming c;
       val classes' = classes |> Sorts.add_class pp (c', cs');
     in ((space', classes'), default, types) end);
 
@@ -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,23 +555,11 @@
 
 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) =
+fun new_decl naming tags (c, decl) 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;
+    val (_, types') = NameSpace.define true naming (c, (decl, tags')) types;
+  in types' end;
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let
@@ -585,38 +569,34 @@
   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)) =>
@@ -635,7 +615,7 @@
     val space' = NameSpace.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' = NameSpace.merge_tables (types1, types2);
   in build_tsig ((space', classes'), default', types') end;
 
 end;