Seq.maps;
authorwenzelm
Tue Sep 13 22:19:28 2005 +0200 (2005-09-13)
changeset 173448b2f56aff711
parent 17343 098db1bc1e59
child 17345 9ea1e2179786
Seq.maps;
src/Pure/tctical.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/tctical.ML	Tue Sep 13 22:19:27 2005 +0200
     1.2 +++ b/src/Pure/tctical.ML	Tue Sep 13 22:19:28 2005 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4  (*** LCF-style tacticals ***)
     1.5  
     1.6  (*the tactical THEN performs one tactic followed by another*)
     1.7 -fun (tac1 THEN tac2) st = Seq.flat (Seq.map tac2 (tac1 st));
     1.8 +fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st);
     1.9  
    1.10  
    1.11  (*The tactical ORELSE uses the first tactic that returns a nonempty sequence.
    1.12 @@ -116,9 +116,8 @@
    1.13  *)
    1.14  fun (tac THEN_ELSE (tac1, tac2)) st =
    1.15      case Seq.pull(tac st) of
    1.16 -        NONE    => tac2 st              (*failed; try tactic 2*)
    1.17 -      | seqcell => Seq.flat       (*succeeded; use tactic 1*)
    1.18 -                    (Seq.map tac1 (Seq.make(fn()=> seqcell)));
    1.19 +        NONE    => tac2 st                                   (*failed; try tactic 2*)
    1.20 +      | seqcell => Seq.maps tac1 (Seq.make(fn()=> seqcell)); (*succeeded; use tactic 1*)
    1.21  
    1.22  
    1.23  (*Versions for combining tactic-valued functions, as in
    1.24 @@ -383,8 +382,7 @@
    1.25      fun restore th = Seq.hd (bicompose false (false, th, nprems_of th) 1
    1.26        (Thm.incr_indexes (#maxidx (rep_thm th) + 1) Drule.rev_triv_goal));
    1.27      fun next st' = bicompose false (false, restore st', nprems_of st') i st;
    1.28 -  in  Seq.flat (Seq.map next (tac thm))
    1.29 -  end;
    1.30 +  in Seq.maps next (tac thm) end;
    1.31  
    1.32  fun SELECT_GOAL tac i st =
    1.33    let val np = nprems_of st
    1.34 @@ -492,8 +490,7 @@
    1.35        (*function to replace the current subgoal*)
    1.36        fun next st = bicompose false (false, relift st, nprems_of st)
    1.37                      i state
    1.38 -  in  Seq.flat (Seq.map next (tacf subprems st0))
    1.39 -  end;
    1.40 +  in Seq.maps next (tacf subprems st0) end;
    1.41  end;
    1.42  
    1.43  fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf);
     2.1 --- a/src/Pure/unify.ML	Tue Sep 13 22:19:27 2005 +0200
     2.2 +++ b/src/Pure/unify.ML	Tue Sep 13 22:19:28 2005 +0200
     2.3 @@ -338,8 +338,7 @@
     2.4  		 (env, dpairs)));
     2.5  	(*Produce sequence of all possible ways of copying the arg list*)
     2.6      fun copyargs [] = Seq.cons( ([],ed), Seq.empty)
     2.7 -      | copyargs (uarg::uargs) =
     2.8 -	    Seq.flat (Seq.map (copycons uarg) (copyargs uargs));
     2.9 +      | copyargs (uarg::uargs) = Seq.maps (copycons uarg) (copyargs uargs);
    2.10      val (uhead,uargs) = strip_comb u;
    2.11      val base = body_type env (fastype env (rbinder,uhead));
    2.12      fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');