--- a/src/HOL/Tools/datatype_codegen.ML Tue Jul 25 16:43:32 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Jul 25 16:43:33 2006 +0200
@@ -18,7 +18,7 @@
val get_datatype_mut_specs: theory -> string list
-> ((string * sort) list * (string * (string * typ list) list) list)
val get_datatype_arities: theory -> string list -> sort
- -> (string * (((string * sort list) * sort) * term list)) list option
+ -> (string * (((string * sort list) * sort) * term list)) list option
val prove_arities: (thm list -> tactic) -> string list -> sort
-> (((string * sort list) * sort) list -> (string * term list) list
-> ((bstring * attribute list) * term) list) -> theory -> theory