tuned;

--- a/src/HOL/Tools/datatype_aux.ML	Wed Mar 01 16:40:14 2000 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Wed Mar 01 20:48:57 2000 +0100
@@ -154,8 +154,7 @@
 
 type datatype_info =
   {index : int,
-   descr : (int * (string * dtyp list *
-     (string * dtyp list) list)) list,
+   descr : (int * (string * dtyp list * (string * dtyp list) list)) list,
    rec_names : string list,
    rec_rewrites : thm list,
    case_name : string,