# HG changeset patch
# User berghofe
# Date 1146152921 -7200
# Node ID 4441b637871ba1f671eb8315b2667a66c954988d
# Parent  8bd2c840458ec5f82d960a780f56e67adc27f592
SplitAt -> chop

diff -r 8bd2c840458e -r 4441b637871b 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';