# HG changeset patch
# User berghofe
# Date 1122026111 -7200
# Node ID d649ff14096a821b0d3d75f4ebde7cba0bb8b027
# Parent  e294033d1c0fbcb326babc323a84391ac170f397
Tuned comment.

diff -r e294033d1c0f -r d649ff14096a src/HOL/Tools/datatype_aux.ML
--- 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 =