src/Pure/tctical.ML

 
 
 (*** 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.
   Like in LCF, ORELSE commits to either tac1 or tac2 immediately.
   Does not backtrack to tac2 if tac1 was initially chosen. *)

         tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
         tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
 *)
 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
      SOMEGOAL (resolve_tac rls THEN' assume_tac) *)
 fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x;

   let
     val thm = Drule.mk_triv_goal (adjust_maxidx (List.nth (cprems_of st, i-1)));
     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
   in  if 1<=i andalso i<=np then
           (*If only one subgoal, then just apply tactic*)

       val subprems = map (forall_elim_vars 0) hypths
       and st0 = trivial (cterm concl)
       (*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);
 
 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)