src/HOL/Tools/inductive_codegen.ML

   val name = "HOL/inductive_codegen";
   type T = thm list Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val prep_ext = I;
-  val merge = Symtab.merge_multi eq_thm;
+  val merge = Symtab.merge_multi Drule.eq_thm_prop;
   fun print _ _ = ();
 end;
 
 structure CodegenData = TheoryDataFun(CodegenArgs);