diff -r 098db1bc1e59 -r 8b2f56aff711 src/Pure/unify.ML
--- 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');