src/Pure/ML/ml_env.ML
changeset 33519 e31a85f92ce9
parent 31470 01e7a8bb9e5b
child 36163 823c9400eb62
--- a/src/Pure/ML/ml_env.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/ML/ml_env.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -16,7 +16,7 @@
 
 (* context data *)
 
-structure Env = GenericDataFun
+structure Env = Generic_Data
 (
   type T =
     ML_Name_Space.valueVal Symtab.table *
@@ -27,7 +27,7 @@
     ML_Name_Space.functorVal Symtab.table;
   val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
   val extend = I;
-  fun merge _
+  fun merge
    ((val1, type1, fixity1, structure1, signature1, functor1),
     (val2, type2, fixity2, structure2, signature2, functor2)) : T =
     (Symtab.merge (K true) (val1, val2),