# HG changeset patch
# User wenzelm
# Date 952647217 -3600
# Node ID 4b39358f9810fdbbea1a8f98e9afbb2b3b06d48b
# Parent  a8a0411a8e8c1108f2bb5ffef4111573674eedd6
type descr;

diff -r a8a0411a8e8c -r 4b39358f9810 src/HOL/Tools/datatype_aux.ML
--- 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,