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