src/HOL/Tools/inductive.ML

   end;
 
 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));
 );
 
 val get_inductives = InductiveData.get o Context.Proof;