diff -r 663108ee4eef -r fe474e69e603 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Fri Dec 29 03:57:01 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Dec 29 12:11:00 2006 +0100
@@ -26,7 +26,7 @@
     -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
   val get_codetypes_arities: theory -> (string * bool) list -> sort
     -> (string * (((string * sort list) * sort) * term list)) list option
-  val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
+  val prove_codetypes_arities: tactic -> (string * bool) list -> sort
     -> (((string * sort list) * sort) list -> (string * term list) list -> theory
     -> ((bstring * attribute list) * term) list * theory)
     -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
@@ -612,7 +612,7 @@
         |> not (null arities) ? (
             f arities css
             #-> (fn defs =>
-              ClassPackage.prove_instance_arity tac arities ("", []) defs
+              ClassPackage.prove_instance_arity tac arities defs
             #> after_qed arities css))
       end;
 
@@ -631,7 +631,7 @@
         CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
       end;
   in
-    prove_codetypes_arities (K (ClassPackage.intro_classes_tac []))
+    prove_codetypes_arities (ClassPackage.intro_classes_tac [])
       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
       [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
   end;