# HG changeset patch
# User wenzelm
# Date 1131652638 -3600
# Node ID 7921f41165cf4ff717726f12209241919db3ba52
# Parent  31634a2af39e4248d382a19d85cf7073143901e1
curried multiply;

diff -r 31634a2af39e -r 7921f41165cf src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Nov 10 20:57:17 2005 +0100
+++ b/src/Pure/library.ML	Thu Nov 10 20:57:18 2005 +0100
@@ -113,7 +113,7 @@
   val get_first: ('a -> 'b option) -> 'a list -> 'b option
   val separate: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
-  val multiply: 'a list * 'a list list -> 'a list 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
@@ -612,8 +612,8 @@
 fun translate_string f = String.translate (f o String.str);
 
 (*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
-fun multiply ([], _) = []
-  | multiply (x :: xs, yss) = map (cons x) yss @ multiply (xs, yss);
+fun multiply [] _ = []
+  | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
 
 (*direct product*)
 fun product _ [] = []