--- a/src/Pure/unify.ML Tue Sep 13 22:19:27 2005 +0200
+++ b/src/Pure/unify.ML Tue Sep 13 22:19:28 2005 +0200
@@ -338,8 +338,7 @@
(env, dpairs)));
(*Produce sequence of all possible ways of copying the arg list*)
fun copyargs [] = Seq.cons( ([],ed), Seq.empty)
- | copyargs (uarg::uargs) =
- Seq.flat (Seq.map (copycons uarg) (copyargs uargs));
+ | copyargs (uarg::uargs) = Seq.maps (copycons uarg) (copyargs uargs);
val (uhead,uargs) = strip_comb u;
val base = body_type env (fastype env (rbinder,uhead));
fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');