src/Pure/library.ML
changeset 18549 5308a6ea3b96
parent 18514 0cec730b3942
child 18681 3020496cff28
     1.1 --- a/src/Pure/library.ML	Tue Jan 03 00:06:30 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Jan 03 11:31:15 2006 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     1.5    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     1.6    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
     1.7 -  val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
     1.8 +  val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
     1.9    val splitAt: int * 'a list -> 'a list * 'a list
    1.10    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    1.11    val nth: 'a list -> int -> 'a
    1.12 @@ -607,8 +607,8 @@
    1.13  fun burrow f xss =
    1.14    unflat xss ((f o flat) xss);
    1.15  
    1.16 -fun burrow_split f xss =
    1.17 -  apsnd (unflat xss) ((f o flat) xss);
    1.18 +fun fold_burrow f xss s =
    1.19 +  apfst (unflat xss) (f (flat xss) s);
    1.20  
    1.21  (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
    1.22    (proc x1; ...; proc xn) for side effects*)