src/Pure/thm.ML
changeset 33955 fff6f11b1f09
parent 33832 cff42395c246
child 33957 e9afca2118d4
--- a/src/Pure/thm.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/thm.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -1457,7 +1457,7 @@
     val short = length iparams - length cs;
     val newnames =
       if short < 0 then error "More names than abstractions!"
-      else Name.variant_list cs (Library.take (short, iparams)) @ cs;
+      else Name.variant_list cs ((uncurry take) (short, iparams)) @ cs;
     val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
     val newBi = Logic.list_rename_params (newnames, Bi);
   in