# HG changeset patch
# User wenzelm
# Date 1191618256 -7200
# Node ID f33ff5fc1f7e4b48fbe4ce4da00bb269059b0abf
# Parent  307b979b1f542d4249f981227cd75ba6e202b02f
added burrow_options;

diff -r 307b979b1f54 -r f33ff5fc1f7e src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Oct 05 23:04:14 2007 +0200
+++ b/src/Pure/library.ML	Fri Oct 05 23:04:16 2007 +0200
@@ -78,6 +78,7 @@
   val flat: 'a list list -> 'a list
   val unflat: 'a list list -> 'b list -> 'b list list
   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
+  val burrow_options: ('a list -> 'b list) -> 'a option list -> 'b option list
   val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
   val maps: ('a -> 'b list) -> 'a list -> 'b list
   val chop: int -> 'a list -> 'a list * 'a list
@@ -493,6 +494,8 @@
 
 fun burrow f xss = unflat xss (f (flat xss));
 
+fun burrow_options f os = map (try hd) (burrow f (map the_list os));
+
 fun fold_burrow f xss s =
   apfst (unflat xss) (f (flat xss) s);