--- a/src/ZF/Tools/cartprod.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/ZF/Tools/cartprod.ML Thu Mar 03 12:43:01 2005 +0100
@@ -96,7 +96,7 @@
(*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*)