diff -r c2ce4797321a -r 7a24d827cba9 Nominal/nominal_basics.ML
--- a/Nominal/nominal_basics.ML	Mon Jul 11 12:23:44 2011 +0100
+++ b/Nominal/nominal_basics.ML	Mon Jul 11 14:02:13 2011 +0200
@@ -4,11 +4,16 @@
   Basic functions for nominal.
 *)
 
+infix 1 ||>>> |>>>
+
 signature NOMINAL_BASIC =
 sig
   val trace: bool Unsynchronized.ref
   val trace_msg: (unit -> string) -> unit
 
+  val |>>> : 'a * ('a -> 'b * 'c) -> 'b list * 'c
+  val ||>>> : ('a list * 'b) * ('b -> 'a * 'b) -> 'a list * 'b
+
   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
@@ -54,6 +59,24 @@
 fun trace_msg msg = if ! trace then tracing (msg ()) else ()
 
 
+infix 1 ||>>> |>>>
+
+fun (x |>>> f) = 
+  let 
+    val (x', y') = f x 
+  in
+    ([x'], y')
+  end
+
+fun (([], y) ||>>> f) = ([], y)  
+  | ((xs, y) ||>>> f) =
+       let
+         val (x', y') = f y
+       in
+         (xs @ [x'], y')
+       end
+
+
 (* orders an AList according to keys - every key needs to be there *)
 fun order eq keys list = 
   map (the o AList.lookup eq list) keys