src/HOL/Tools/transfer.ML

--- a/src/HOL/Tools/transfer.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/transfer.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -25,12 +25,12 @@
 
 type data = simpset * (thm * entry) list;
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = data;
   val empty = (HOL_ss, []);
   val extend  = I;
-  fun merge _ ((ss1, e1), (ss2, e2)) =
+  fun merge ((ss1, e1), (ss2, e2)) : T =
     (merge_ss (ss1, ss2), AList.join Thm.eq_thm (K merge_entry) (e1, e2));
 );