diff -r d0f83a35950e -r 9bd97ed202f7 Nominal/nominal_basics.ML
--- a/Nominal/nominal_basics.ML	Thu Jul 07 16:17:03 2011 +0200
+++ b/Nominal/nominal_basics.ML	Fri Jul 08 05:04:23 2011 +0200
@@ -10,6 +10,7 @@
   val trace_msg: (unit -> string) -> unit
 
   val last2: 'a list -> 'a * 'a
+  val split_triples: ('a * 'b * 'c) list -> ('a list * 'b list * 'c list)
   val split_last2: 'a list -> 'a list * 'a * 'a
   val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
   val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list
@@ -68,6 +69,9 @@
       then remove_dups eq xs 
       else x :: remove_dups eq xs
 
+fun split_triples xs =
+  fold (fn (a, b, c) => fn (axs, bxs, cxs) => (a :: axs, b :: bxs, c :: cxs)) xs ([], [], [])
+
 fun last2 [] = raise Empty
   | last2 [_] = raise Empty
   | last2 [x, y] = (x, y)