--- a/src/HOL/Nominal/nominal_datatype.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Nov 25 09:13:46 2009 +0100
@@ -766,8 +766,8 @@
Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
val recTs = get_rec_types descr'' sorts;
- val newTs' = (uncurry take) (length new_type_names, recTs');
- val newTs = (uncurry take) (length new_type_names, recTs);
+ val newTs' = take (length new_type_names) recTs';
+ val newTs = take (length new_type_names) recTs;
val full_new_type_names = map (Sign.full_bname thy) new_type_names;