--- a/src/Pure/General/basics.ML Sat Dec 23 19:08:35 2023 +0100
+++ b/src/Pure/General/basics.ML Sun Dec 24 11:13:33 2023 +0100
@@ -45,6 +45,7 @@
val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
+ val fold_maps: ('a -> 'b -> 'c list * 'b) -> 'a list -> 'b -> 'c list * 'b
end;
structure Basics: BASICS =
@@ -130,6 +131,13 @@
val (xs', y'') = fold_map f xs y';
in (x' :: xs', y'') end;
+fun fold_maps _ [] y = ([], y)
+ | fold_maps f (x :: xs) y =
+ let
+ val (x', y') = f x y;
+ val (xs', y'') = fold_maps f xs y';
+ in (x' @ xs', y'') end;
+
end;
open Basics;