diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -136,12 +136,12 @@
 type inductive_info =
   {names: string list, coind: bool} * inductive_result;
 
-structure InductiveData = GenericDataFun
+structure InductiveData = Generic_Data
 (
   type T = inductive_info Symtab.table * thm list;
   val empty = (Symtab.empty, []);
   val extend = I;
-  fun merge _ ((tab1, monos1), (tab2, monos2)) =
+  fun merge ((tab1, monos1), (tab2, monos2)) : T =
     (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2));
 );