# 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,