src/Pure/Isar/attrib.ML
changeset 33522 737589bb9bb8
parent 33368 b1cf34f1855c
child 33666 e49bfeb0d822
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -65,13 +65,12 @@
     1.4  
     1.5  (* theory data *)
     1.6  
     1.7 -structure Attributes = TheoryDataFun
     1.8 +structure Attributes = Theory_Data
     1.9  (
    1.10    type T = ((src -> attribute) * string) Name_Space.table;
    1.11    val empty : T = Name_Space.empty_table "attribute";
    1.12 -  val copy = I;
    1.13    val extend = I;
    1.14 -  fun merge _ tables : T = Name_Space.merge_tables tables;
    1.15 +  fun merge data : T = Name_Space.merge_tables data;
    1.16  );
    1.17  
    1.18  fun print_attributes thy =
    1.19 @@ -321,13 +320,12 @@
    1.20  
    1.21  (* naming *)
    1.22  
    1.23 -structure Configs = TheoryDataFun
    1.24 +structure Configs = Theory_Data
    1.25  (
    1.26    type T = Config.value Config.T Symtab.table;
    1.27    val empty = Symtab.empty;
    1.28 -  val copy = I;
    1.29    val extend = I;
    1.30 -  fun merge _ = Symtab.merge (K true);
    1.31 +  fun merge data = Symtab.merge (K true) data;
    1.32  );
    1.33  
    1.34  fun print_configs ctxt =