# HG changeset patch
# User haftmann
# Date 1153838613 -7200
# Node ID 03a8d7c070d3af9abb3114330bd772f84d8cb2d6
# Parent  1be8b181dafa7422be1f3c2604c7b3e1545c069d
fixed typo

diff -r 1be8b181dafa -r 03a8d7c070d3 src/HOL/Tools/datatype_codegen.ML
--- 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