tuned signature;
observe coding conventions of this file;

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Sat Oct 17 14:51:30 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sat Oct 17 15:42:36 2009 +0200
@@ -6,14 +6,32 @@
 
 signature DATATYPE_COMMON =
 sig
-  type config
+  type config = {strict : bool, quiet : bool}
   val default_config : config
   datatype dtyp =
       DtTFree of string
-    | DtType of string * (dtyp list)
-    | DtRec of int;
-  type descr
-  type info
+    | DtType of string * dtyp list
+    | DtRec of int
+  type descr = (int * (string * dtyp list * (string * dtyp list) list)) list
+  type info =
+   {index : int,
+    alt_names : string list option,
+    descr : descr,
+    sorts : (string * sort) list,
+    inject : thm list,
+    distinct : thm list,
+    induct : thm,
+    inducts : thm list,
+    exhaust : thm,
+    nchotomy : thm,
+    rec_names : string list,
+    rec_rewrites : thm list,
+    case_name : string,
+    case_rewrites : thm list,
+    case_cong : thm,
+    weak_case_cong : thm,
+    split : thm,
+    split_asm: thm}
 end
 
 signature DATATYPE_AUX =
@@ -68,11 +86,11 @@
 
 (* datatype option flags *)
 
-type config = { strict: bool, quiet: bool };
-val default_config : config =
-  { strict = true, quiet = false };
-fun message ({ quiet, ...} : config) s =
-  if quiet then () else writeln s;
+type config = {strict : bool, quiet : bool};
+val default_config : config = {strict = true, quiet = false};
+
+fun message ({quiet = true, ...} : config) s = writeln s
+  | message _ _ = ();
 
 
 (* store theorems in theory *)