src/Pure/library.ML
changeset 30190 479806475f3c
parent 29882 29154e67731d
child 30558 2ef9892114fd
     1.1 --- a/src/Pure/library.ML	Sun Mar 01 16:48:06 2009 +0100
     1.2 +++ b/src/Pure/library.ML	Sun Mar 01 23:36:12 2009 +0100
     1.3 @@ -76,7 +76,6 @@
     1.4    val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
     1.5    val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a
     1.6    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     1.7 -  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     1.8    val flat: 'a list list -> 'a list
     1.9    val unflat: 'a list list -> 'b list -> 'b list list
    1.10    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
    1.11 @@ -238,6 +237,7 @@
    1.12    include BASIC_LIBRARY
    1.13    val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
    1.14    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    1.15 +  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.16    val take: int * 'a list -> 'a list
    1.17    val drop: int * 'a list -> 'a list
    1.18    val last_elem: 'a list -> 'a