src/Pure/library.ML
changeset 24864 f33ff5fc1f7e
parent 24846 d8ff870a11ff
child 24979 783bf93c8f92
     1.1 --- a/src/Pure/library.ML	Fri Oct 05 23:04:14 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Oct 05 23:04:16 2007 +0200
     1.3 @@ -78,6 +78,7 @@
     1.4    val flat: 'a list list -> 'a list
     1.5    val unflat: 'a list list -> 'b list -> 'b list list
     1.6    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
     1.7 +  val burrow_options: ('a list -> 'b list) -> 'a option list -> 'b option list
     1.8    val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
     1.9    val maps: ('a -> 'b list) -> 'a list -> 'b list
    1.10    val chop: int -> 'a list -> 'a list * 'a list
    1.11 @@ -493,6 +494,8 @@
    1.12  
    1.13  fun burrow f xss = unflat xss (f (flat xss));
    1.14  
    1.15 +fun burrow_options f os = map (try hd) (burrow f (map the_list os));
    1.16 +
    1.17  fun fold_burrow f xss s =
    1.18    apfst (unflat xss) (f (flat xss) s);
    1.19