src/Pure/Isar/attrib.ML
changeset 33522 737589bb9bb8
parent 33368 b1cf34f1855c
child 33666 e49bfeb0d822
--- a/src/Pure/Isar/attrib.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -65,13 +65,12 @@
 
 (* theory data *)
 
-structure Attributes = TheoryDataFun
+structure Attributes = Theory_Data
 (
   type T = ((src -> attribute) * string) Name_Space.table;
   val empty : T = Name_Space.empty_table "attribute";
-  val copy = I;
   val extend = I;
-  fun merge _ tables : T = Name_Space.merge_tables tables;
+  fun merge data : T = Name_Space.merge_tables data;
 );
 
 fun print_attributes thy =
@@ -321,13 +320,12 @@
 
 (* naming *)
 
-structure Configs = TheoryDataFun
+structure Configs = Theory_Data
 (
   type T = Config.value Config.T Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ = Symtab.merge (K true);
+  fun merge data = Symtab.merge (K true) data;
 );
 
 fun print_configs ctxt =