src/ZF/Tools/cartprod.ML

   | ap_split T T3 u = u;
 
 (*Makes a nested tuple from a list, following the product type structure*)
 fun mk_tuple pair (Type("*", [T1,T2])) tms = 
         pair $ (mk_tuple pair T1 tms)
-             $ (mk_tuple pair T2 (drop (length (factors T1), tms)))
+             $ (mk_tuple pair T2 (Library.drop (length (factors T1), tms)))
   | mk_tuple pair T (t::_) = t;
 
 (*Attempts to remove occurrences of split, and pair-valued parameters*)
 val remove_split = rewrite_rule [Pr.split_eq];