SplitAt -> chop
authorberghofe
Thu, 27 Apr 2006 17:48:41 +0200
changeset 19489 4441b637871b
parent 19488 8bd2c840458e
child 19490 bf7f8347174a
SplitAt -> chop
src/HOL/Nominal/nominal_package.ML
--- 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';