# HG changeset patch
# User haftmann
# Date 1222327685 -7200
# Node ID 3cb64932ac77a6a403ef9f1a4b730c16d4283272
# Parent  b8390cd56b8fdab1f663c832a95ceafb1dfc48a9
burrow_fst

diff -r b8390cd56b8f -r 3cb64932ac77 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Sep 25 09:28:03 2008 +0200
+++ b/src/Pure/library.ML	Thu Sep 25 09:28:05 2008 +0200
@@ -84,6 +84,7 @@
   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 burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) 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 filter: ('a -> bool) -> 'a list -> 'a list
@@ -605,6 +606,8 @@
   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
 val split_list = ListPair.unzip;
 
+fun burrow_fst f xs = split_list xs |>> f |> op ~~;
+
 
 (* prefixes, suffixes *)