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