diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -193,8 +193,7 @@
 fun mk_pat (c,l) =
   let val L = length (binder_types (type_of c))
       fun build (prfx,tag,plist) =
-          let val args   = Library.take (L,plist)
-              and plist' = Library.drop(L,plist)
+          let val (args, plist') = chop L plist
           in (prfx,tag,list_comb(c,args)::plist') end
   in map build l end;