# HG changeset patch
# User wenzelm
# Date 951940137 -3600
# Node ID df7dccddc3de5614447f6d79ab1a01e9edc42d81
# Parent  64b67ed25a5990b5b46a92972187bc1600fabd91
tuned;

diff -r 64b67ed25a59 -r df7dccddc3de src/HOL/Tools/datatype_aux.ML
--- 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,