discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
authorwenzelm
Sat Mar 03 22:27:30 2012 +0100 (2012-03-03)
changeset 467794f298836018b
parent 46778 7cc567fd2789
child 46793 3bbc156823dd
discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Sat Mar 03 22:17:52 2012 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Mar 03 22:27:30 2012 +0100
     1.3 @@ -62,7 +62,6 @@
     1.4    val the_single: 'a list -> 'a
     1.5    val singleton: ('a list -> 'b list) -> 'a -> 'b
     1.6    val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c
     1.7 -  val apply: ('a -> 'a) list -> 'a -> 'a
     1.8    val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option
     1.9    val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
    1.10    val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.11 @@ -229,7 +228,6 @@
    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  end;
    1.17  
    1.18  structure Library: LIBRARY =
    1.19 @@ -334,9 +332,6 @@
    1.20  
    1.21  fun yield_singleton f x = f [x] #>> the_single;
    1.22  
    1.23 -fun apply [] x = x
    1.24 -  | apply (f :: fs) x = apply fs (f x);
    1.25 -
    1.26  fun perhaps_apply funs arg =
    1.27    let
    1.28      fun app [] res = res
    1.29 @@ -386,16 +381,6 @@
    1.30              | itr (x::l) = f(x, itr l)
    1.31        in  itr l  end;
    1.32  
    1.33 -fun foldl_map f =
    1.34 -  let
    1.35 -    fun fold_aux (x, []) = (x, [])
    1.36 -      | fold_aux (x, y :: ys) =
    1.37 -          let
    1.38 -            val (x', y') = f (x, y);
    1.39 -            val (x'', ys') = fold_aux (x', ys);
    1.40 -          in (x'', y' :: ys') end;
    1.41 -  in fold_aux end;
    1.42 -
    1.43  
    1.44  (* basic list functions *)
    1.45