src/HOL/Nominal/nominal_package.ML
changeset 19489 4441b637871b
parent 19403 5c15cd397a82
child 19494 2e909d5309f4
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Thu Apr 27 17:48:17 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Apr 27 17:48:41 2006 +0200
     1.3 @@ -671,7 +671,7 @@
     1.4                 (index, constrs2))
     1.5               end) descr);
     1.6  
     1.7 -    val (descr1, descr2) = splitAt (length new_type_names, descr'');
     1.8 +    val (descr1, descr2) = chop (length new_type_names) descr'';
     1.9      val descr' = [descr1, descr2];
    1.10  
    1.11      val typ_of_dtyp' = replace_types' o typ_of_dtyp descr sorts';