# HG changeset patch
# User wenzelm
# Date 1703412813 -3600
# Node ID e8d7b7d5390d8f7a78b1a2bea61e709fad0700ce
# Parent  3ef7606a0d11a99280e59c8d60b1c75e00723692
more operations;

diff -r 3ef7606a0d11 -r e8d7b7d5390d src/Pure/General/basics.ML
--- 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;