--- a/src/HOL/Tools/datatype_aux.ML Thu Mar 09 22:58:23 2000 +0100
+++ b/src/HOL/Tools/datatype_aux.ML Fri Mar 10 01:13:37 2000 +0100
@@ -34,7 +34,7 @@
DtTFree of string
| DtType of string * (dtyp list)
| DtRec of int;
-
+ type descr
type datatype_info
exception Datatype
@@ -152,9 +152,11 @@
(* information about datatypes *)
+type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
+
type datatype_info =
{index : int,
- descr : (int * (string * dtyp list * (string * dtyp list) list)) list,
+ descr : descr,
rec_names : string list,
rec_rewrites : thm list,
case_name : string,