eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;

--- a/src/Pure/Isar/attrib.ML	Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Oct 24 19:20:03 2009 +0200
@@ -67,27 +67,25 @@
 
 structure Attributes = TheoryDataFun
 (
-  type T = (((src -> attribute) * string) * stamp) NameSpace.table;
+  type T = ((src -> attribute) * string) NameSpace.table;
   val empty = NameSpace.empty_table;
   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 = NameSpace.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.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 NameSpace.define true (Sign.naming_of thy) (name, (att, comment)));
 
 
 (* name space *)
@@ -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;
 

--- a/src/Pure/Isar/locale.ML	Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Oct 24 19:20:03 2009 +0200
@@ -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 (NameSpace.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),

--- a/src/Pure/Isar/method.ML	Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/Isar/method.ML	Sat Oct 24 19:20:03 2009 +0200
@@ -322,27 +322,25 @@
 
 structure Methods = TheoryDataFun
 (
-  type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
+  type T = ((src -> Proof.context -> method) * string) NameSpace.table;
   val empty = NameSpace.empty_table;
   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 = NameSpace.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.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 NameSpace.define true (Sign.naming_of thy) (name, (meth, comment)));
 
 
 (* get methods *)
@@ -357,7 +355,7 @@
       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;
 

--- a/src/Pure/codegen.ML	Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/codegen.ML	Sat Oct 24 19:20:03 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;
 

--- a/src/Pure/consts.ML	Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/consts.ML	Sat Oct 24 19:20:03 2009 +0200
@@ -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) NameSpace.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 =
@@ -221,13 +221,6 @@
 
 (** 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) =>
@@ -236,12 +229,13 @@
 
 (* 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 tags' = tags |> Position.default_properties (Position.thread_data ());
+      val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
+      val (_, decls') = decls |> NameSpace.define true naming (b, (decl, NONE));
+    in (decls', constraints, rev_abbrevs) end);
 
 
 (* constraints *)
@@ -278,7 +272,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)
@@ -294,7 +288,7 @@
         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 ()));
+          |> NameSpace.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)
@@ -319,8 +313,7 @@
    (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' = NameSpace.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;

--- a/src/Pure/display.ML	Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/display.ML	Sat Oct 24 19:20:03 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, [])));
 

--- a/src/Pure/simplifier.ML	Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/simplifier.ML	Sat Oct 24 19:20:03 2009 +0200
@@ -143,9 +143,6 @@
 
 (** named simprocs **)
 
-fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
-
-
 (* data *)
 
 structure Simprocs = GenericDataFun
@@ -153,8 +150,7 @@
   type T = simproc NameSpace.table;
   val empty = NameSpace.empty_table;
   val extend = I;
-  fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
-    handle Symtab.DUP dup => err_dup_simproc dup;
+  fun merge _ simprocs = NameSpace.merge_tables simprocs;
 );
 
 
@@ -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 NameSpace.define true naming (b', simproc'))
         #> map_ss (fn ss => ss addsimprocs [simproc'])
       end)
   end;

--- a/src/Pure/theory.ML	Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/theory.ML	Sat Oct 24 19:20:03 2009 +0200
@@ -86,8 +86,6 @@
 
 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;
@@ -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 NameSpace.define true (Sign.naming_of thy)) axms axioms;
   in axioms' end);
 
 in

--- a/src/Pure/thm.ML	Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/thm.ML	Sat Oct 24 19:20:03 2009 +0200
@@ -1724,16 +1724,13 @@
 
 (* authentic derivation names *)
 
-fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
-
 structure Oracles = TheoryDataFun
 (
-  type T = serial NameSpace.table;
+  type T = unit NameSpace.table;
   val empty = NameSpace.empty_table;
   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 = NameSpace.merge_tables oracles;
 );
 
 val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
@@ -1741,8 +1738,7 @@
 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') = NameSpace.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;