diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Fri Jun 17 18:33:03 2005 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jun 17 18:33:05 2005 +0200
@@ -18,8 +18,8 @@
 
 (**** theory data ****)
 
-structure CodegenArgs =
-struct
+structure CodegenData = TheoryDataFun
+(struct
   val name = "HOL/inductive_codegen";
   type T =
     {intros : thm list Symtab.table,
@@ -28,16 +28,15 @@
   val empty =
     {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
   val copy = I;
-  val prep_ext = I;
-  fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
+  val extend = I;
+  fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
     {intros=intros2, graph=graph2, eqns=eqns2}) =
     {intros = Symtab.merge_multi Drule.eq_thm_prop (intros1, intros2),
      graph = Graph.merge (K true) (graph1, graph2),
      eqns = Symtab.merge_multi Drule.eq_thm_prop (eqns1, eqns2)};
   fun print _ _ = ();
-end;
+end);
 
-structure CodegenData = TheoryDataFun(CodegenArgs);
 
 fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
   string_of_thm thm);