author | berghofe |
Thu, 27 Apr 2006 17:48:41 +0200 | |
changeset 19489 | 4441b637871b |
parent 19488 | 8bd2c840458e |
child 19490 | bf7f8347174a |
--- a/src/HOL/Nominal/nominal_package.ML Thu Apr 27 17:48:17 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Thu Apr 27 17:48:41 2006 +0200 @@ -671,7 +671,7 @@ (index, constrs2)) end) descr); - val (descr1, descr2) = splitAt (length new_type_names, descr''); + val (descr1, descr2) = chop (length new_type_names) descr''; val descr' = [descr1, descr2]; val typ_of_dtyp' = replace_types' o typ_of_dtyp descr sorts';