--- 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;