diff -r d17fadc20507 -r 25fb0dbe9f13 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Wed Dec 22 10:32:01 2010 +0000
+++ b/Nominal/nominal_library.ML	Wed Dec 22 12:17:49 2010 +0000
@@ -9,8 +9,9 @@
   val last2: 'a list -> 'a * 'a
   val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
   val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
-  val partitions: 'a list -> int list -> 'a list list
+  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
   val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list
+  
 
   val is_true: term -> bool
  
@@ -138,14 +139,8 @@
   | last2 [x, y] = (x, y)
   | last2 (_ :: xs) = last2 xs
 
-(* partitions a set according to the numbers in the int list *)
-fun partitions [] [] = []
-  | partitions xs (i :: js) = 
-      let
-        val (head, tail) = chop i xs
-      in
-        head :: partitions tail js
-      end
+fun map4 _ [] [] [] [] = []
+  | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
 
 fun split_filter f [] = ([], [])
   | split_filter f (x :: xs) =