diff -r 96f9e6402403 -r 4839a704939a src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Aug 10 10:25:00 2009 +0200
+++ b/src/Pure/library.ML	Mon Aug 10 12:24:47 2009 +0200
@@ -109,6 +109,7 @@
   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 map_transpose: ('a list -> 'b) -> 'a list list -> 'b list
   val separate: 'a -> 'a list -> 'a list
   val surround: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
@@ -929,6 +930,17 @@
   in dups end;
 
 
+(* matrices *)
+
+fun map_transpose f xss =
+  let
+    val n = case distinct (op =) (map length xss)
+     of [] => 0
+      | [n] => n
+      | _ => raise UnequalLengths;
+  in map (fn m => f (map (fn xs => nth xs m) xss)) (0 upto n - 1) end;
+
+
 
 (** lists as multisets **)