diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon May 07 00:49:59 2007 +0200
@@ -22,8 +22,7 @@
   Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
 
 structure CodegenData = TheoryDataFun
-(struct
-  val name = "HOL/inductive_codegen";
+(
   type T =
     {intros : (thm * (string * int)) list Symtab.table,
      graph : unit Graph.T,
@@ -37,8 +36,7 @@
     {intros = merge_rules (intros1, intros2),
      graph = Graph.merge (K true) (graph1, graph2),
      eqns = merge_rules (eqns1, eqns2)};
-  fun print _ _ = ();
-end);
+);
 
 
 fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
@@ -653,7 +651,6 @@
 
 val setup =
   add_codegen "inductive" inductive_codegen #>
-  CodegenData.init #>
   add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
     Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);