src/HOL/Nominal/nominal_datatype.ML
changeset 33955 fff6f11b1f09
parent 33726 0878aecbf119
child 33957 e9afca2118d4
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -766,8 +766,8 @@
     1.4        Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
     1.5  
     1.6      val recTs = get_rec_types descr'' sorts;
     1.7 -    val newTs' = Library.take (length new_type_names, recTs');
     1.8 -    val newTs = Library.take (length new_type_names, recTs);
     1.9 +    val newTs' = (uncurry take) (length new_type_names, recTs');
    1.10 +    val newTs = (uncurry take) (length new_type_names, recTs);
    1.11  
    1.12      val full_new_type_names = map (Sign.full_bname thy) new_type_names;
    1.13