src/HOL/Tools/TFL/tfl.ML
changeset 33955 fff6f11b1f09
parent 33339 d41f77196338
child 35232 f588e1169c8b
     1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -193,8 +193,7 @@
     1.4  fun mk_pat (c,l) =
     1.5    let val L = length (binder_types (type_of c))
     1.6        fun build (prfx,tag,plist) =
     1.7 -          let val args   = Library.take (L,plist)
     1.8 -              and plist' = Library.drop(L,plist)
     1.9 +          let val (args, plist') = chop L plist
    1.10            in (prfx,tag,list_comb(c,args)::plist') end
    1.11    in map build l end;
    1.12