changeset 33955 | fff6f11b1f09 |
parent 33339 | d41f77196338 |
child 35232 | f588e1169c8b |
--- 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;