Seq.maps;

--- a/src/Pure/tctical.ML	Tue Sep 13 22:19:27 2005 +0200
+++ b/src/Pure/tctical.ML	Tue Sep 13 22:19:28 2005 +0200
@@ -86,7 +86,7 @@
 (*** LCF-style tacticals ***)
 
 (*the tactical THEN performs one tactic followed by another*)
-fun (tac1 THEN tac2) st = Seq.flat (Seq.map tac2 (tac1 st));
+fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st);
 
 
 (*The tactical ORELSE uses the first tactic that returns a nonempty sequence.
@@ -116,9 +116,8 @@
 *)
 fun (tac THEN_ELSE (tac1, tac2)) st =
     case Seq.pull(tac st) of
-        NONE    => tac2 st              (*failed; try tactic 2*)
-      | seqcell => Seq.flat       (*succeeded; use tactic 1*)
-                    (Seq.map tac1 (Seq.make(fn()=> seqcell)));
+        NONE    => tac2 st                                   (*failed; try tactic 2*)
+      | seqcell => Seq.maps tac1 (Seq.make(fn()=> seqcell)); (*succeeded; use tactic 1*)
 
 
 (*Versions for combining tactic-valued functions, as in
@@ -383,8 +382,7 @@
     fun restore th = Seq.hd (bicompose false (false, th, nprems_of th) 1
       (Thm.incr_indexes (#maxidx (rep_thm th) + 1) Drule.rev_triv_goal));
     fun next st' = bicompose false (false, restore st', nprems_of st') i st;
-  in  Seq.flat (Seq.map next (tac thm))
-  end;
+  in Seq.maps next (tac thm) end;
 
 fun SELECT_GOAL tac i st =
   let val np = nprems_of st
@@ -492,8 +490,7 @@
       (*function to replace the current subgoal*)
       fun next st = bicompose false (false, relift st, nprems_of st)
                     i state
-  in  Seq.flat (Seq.map next (tacf subprems st0))
-  end;
+  in Seq.maps next (tacf subprems st0) end;
 end;
 
 fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf);

--- 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');