src/Pure/library.ML
changeset 16654 d964cbaa6c1c
parent 16535 86c9eada525b
child 16676 671bd433b9eb
     1.1 --- a/src/Pure/library.ML	Fri Jul 01 14:41:57 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Jul 01 14:41:58 2005 +0200
     1.3 @@ -450,18 +450,27 @@
     1.4  
     1.5  (* fold *)
     1.6  
     1.7 -fun fold _ [] y = y
     1.8 -  | fold f (x :: xs) y = fold f xs (f x y);
     1.9 -
    1.10 -fun fold_rev _ [] y = y
    1.11 -  | fold_rev f (x :: xs) y = f x (fold_rev f xs y);
    1.12 +fun fold f =
    1.13 +  let
    1.14 +    fun fold_aux [] y = y
    1.15 +      | fold_aux (x :: xs) y = fold_aux xs (f x y);
    1.16 +  in fold_aux end;
    1.17  
    1.18 -fun foldl_map _ (x, []) = (x, [])
    1.19 -  | foldl_map f (x, y :: ys) =
    1.20 -      let
    1.21 -        val (x', y') = f (x, y);
    1.22 -        val (x'', ys') = foldl_map f (x', ys);
    1.23 -      in (x'', y' :: ys') end;
    1.24 +fun fold_rev f =
    1.25 +  let
    1.26 +    fun fold_aux [] y = y
    1.27 +      | fold_aux (x :: xs) y = f x (fold_aux xs y);
    1.28 +  in fold_aux end;
    1.29 +
    1.30 +fun foldl_map f =
    1.31 +  let
    1.32 +    fun fold_aux (x, []) = (x, [])
    1.33 +      | fold_aux (x, y :: ys) =
    1.34 +          let
    1.35 +            val (x', y') = f (x, y);
    1.36 +            val (x'', ys') = fold_aux (x', ys);
    1.37 +          in (x'', y' :: ys') end;
    1.38 +  in fold_aux end;
    1.39  
    1.40  (*the following versions of fold are designed to fit nicely with infixes*)
    1.41