src/Pure/config.ML
changeset 33519 e31a85f92ce9
parent 29606 fedb8be05f24
child 36000 5560b2437789
     1.1 --- a/src/Pure/config.ML	Sun Nov 08 16:28:18 2009 +0100
     1.2 +++ b/src/Pure/config.ML	Sun Nov 08 16:30:41 2009 +0100
     1.3 @@ -90,12 +90,12 @@
     1.4  
     1.5  (* context information *)
     1.6  
     1.7 -structure Value = GenericDataFun
     1.8 +structure Value = Generic_Data
     1.9  (
    1.10    type T = value Inttab.table;
    1.11    val empty = Inttab.empty;
    1.12    val extend = I;
    1.13 -  fun merge _ = Inttab.merge (K true);
    1.14 +  fun merge data = Inttab.merge (K true) data;
    1.15  );
    1.16  
    1.17  fun declare global name default =