src/Pure/unify.ML

 	Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
 	    (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
 		 (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');
     (*attempt projection on argument with given typ*)
     val Ts = map (curry (fastype env) rbinder) targs;