src/Pure/library.ML

   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   val get_first: ('a -> 'b option) -> 'a list -> 'b option
   val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+  val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+  val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   val zip_options: 'a list -> 'b option list -> ('a * 'b) list
   val ~~ : 'a list * 'b list -> ('a * 'b) list
   val split_list: ('a * 'b) list -> 'a list * 'b list
   val separate: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
   val multiply: 'a list -> 'a list list -> 'a list list
-  val product: 'a list -> 'b list -> ('a * 'b) list
   val filter: ('a -> bool) -> 'a list -> 'a list
   val filter_out: ('a -> bool) -> 'a list -> 'a list
   val map_filter: ('a -> 'b option) -> 'a list -> 'b list
   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list

   in length list1 = length list2 andalso eq_lst (list1, list2) end;
 
 fun maps f [] = []
   | maps f (x :: xs) = f x @ maps f xs;
 
+(*copy the list preserving elements that satisfy the predicate*)
+val filter = List.filter;
+fun filter_out f = filter (not o f);
+val map_filter = List.mapPartial;
+
 fun chop (0: int) xs = ([], xs)
   | chop _ [] = ([], [])
   | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
 
 (*take the first n elements from a list*)

 (*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
 fun multiply [] _ = []
   | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
 
 (*direct product*)
-fun product _ [] = []
-  | product [] _ = []
-  | product (x :: xs) ys = map (pair x) ys @ product xs ys;
-
-
-(* filter *)
-
-(*copy the list preserving elements that satisfy the predicate*)
-val filter = List.filter;
-fun filter_out f = filter (not o f);
-val map_filter = List.mapPartial;
-
-
-(* lists of pairs *)
+fun map_product f _ [] = []
+  | map_product f [] _ = []
+  | map_product f (x :: xs) ys = map (f x) ys @ map_product f xs ys;
+
+fun fold_product f _ [] z = z
+  | fold_product f [] _ z = z
+  | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys;
+
+(*lists of pairs*)
 
 exception UnequalLengths;
 
 fun map2 _ [] [] = []
   | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys