diff -r 0ee253e66372 -r 1803104d76c9 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Fri Dec 17 00:39:27 2010 +0000
+++ b/Nominal/nominal_library.ML	Fri Dec 17 01:01:44 2010 +0000
@@ -9,6 +9,7 @@
   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 is_true: term -> bool
  
@@ -136,6 +137,17 @@
   | 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 is_true @{term "Trueprop True"} = true
   | is_true _ = false