# HG changeset patch
# User wenzelm
# Date 1146143200 -7200
# Node ID 89484a62184ab422a14ef4c33bc666fadd817bfe
# Parent  55ee839198bdf18f766ef4dfab5cf3f6a5af485d
added map_filter;

diff -r 55ee839198bd -r 89484a62184a src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Thu Apr 27 15:06:39 2006 +0200
+++ b/src/Pure/General/seq.ML	Thu Apr 27 15:06:40 2006 +0200
@@ -29,6 +29,7 @@
   val flat: 'a seq seq -> 'a seq
   val map: ('a -> 'b) -> 'a seq -> 'b seq
   val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
+  val map_filter: ('a -> 'b option) -> 'a seq -> 'b seq
   val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq
   val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq
   val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
@@ -156,6 +157,7 @@
     | SOME (x, xq') => SOME (f x, map f xq')));
 
 fun maps f = flat o map f;
+fun map_filter f = maps (fn x => (case f x of NONE => empty | SOME y => single y));
 
 fun lift f xq y = map (fn x => f x y) xq;
 fun lifts f xq y = maps (fn x => f x y) xq;