src/Pure/Isar/attrib.ML
changeset 33092 c859019d3ac5
parent 31794 71af1fd6a5e4
child 33095 bbd52d2f8696
--- 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;