changeset 33519 | e31a85f92ce9 |
parent 29606 | fedb8be05f24 |
child 36000 | 5560b2437789 |
--- a/src/Pure/config.ML Sun Nov 08 16:28:18 2009 +0100 +++ b/src/Pure/config.ML Sun Nov 08 16:30:41 2009 +0100 @@ -90,12 +90,12 @@ (* context information *) -structure Value = GenericDataFun +structure Value = Generic_Data ( type T = value Inttab.table; val empty = Inttab.empty; val extend = I; - fun merge _ = Inttab.merge (K true); + fun merge data = Inttab.merge (K true) data; ); fun declare global name default =