src/HOL/Tools/type_lifting.ML

--- a/src/HOL/Tools/type_lifting.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/type_lifting.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -27,11 +27,12 @@
 type entry = { mapper: term, variances: (sort * (bool * bool)) list,
   comp: thm, id: thm };
 
-structure Data = Generic_Data(
+structure Data = Generic_Data
+(
   type T = entry list Symtab.table
   val empty = Symtab.empty
-  fun merge (xy : T * T) = Symtab.merge (K true) xy
   val extend = I
+  fun merge data = Symtab.merge (K true) data
 );
 
 val entries = Data.get o Context.Proof;