src/Pure/library.ML
changeset 28347 3cb64932ac77
parent 28157 0435d23deccc
child 28538 3147236326ea
     1.1 --- a/src/Pure/library.ML	Thu Sep 25 09:28:03 2008 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Sep 25 09:28:05 2008 +0200
     1.3 @@ -84,6 +84,7 @@
     1.4    val unflat: 'a list list -> 'b list -> 'b list list
     1.5    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
     1.6    val burrow_options: ('a list -> 'b list) -> 'a option list -> 'b option list
     1.7 +  val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) 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 filter: ('a -> bool) -> 'a list -> 'a list
    1.11 @@ -605,6 +606,8 @@
    1.12    [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
    1.13  val split_list = ListPair.unzip;
    1.14  
    1.15 +fun burrow_fst f xs = split_list xs |>> f |> op ~~;
    1.16 +
    1.17  
    1.18  (* prefixes, suffixes *)
    1.19