# HG changeset patch
# User haftmann
# Date 1206641110 -3600
# Node ID 28310714259201c26ee274f12506af345894d04b
# Parent  faf056ac64c4cad6239c81e72b94d86f9cf3a3df
changed wrong assignement in signature sections

diff -r faf056ac64c4 -r 283107142592 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Mar 27 19:04:42 2008 +0100
+++ b/src/Pure/library.ML	Thu Mar 27 19:05:10 2008 +0100
@@ -109,6 +109,8 @@
   val ~~ : 'a list * 'b list -> ('a * 'b) list
   val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
   val split_list: ('a * 'b) list -> 'a list * 'b list
+  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 separate: 'a -> 'a list -> 'a list
   val surround: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
@@ -158,8 +160,6 @@
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
   val multiply: 'a list -> 'a list list -> 'a list list
-  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
 
   (*lists as sets -- see also Pure/General/ord_list.ML*)
   val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool