Tuned comment.
--- a/src/HOL/Tools/datatype_aux.ML Fri Jul 22 11:54:29 2005 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Fri Jul 22 11:55:11 2005 +0200
@@ -175,7 +175,7 @@
(* information about datatypes *)
-(* index, datatype name, type arguments (DtTFree's), constructor name, types of constructor's arguments *)
+(* index, datatype name, type arguments, constructor name, types of constructor's arguments *)
type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
type datatype_info =