# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1310385733 -7200
# Node ID 7a24d827cba94a8be3769a9664e635512b29f892
# Parent  c2ce4797321a13964e2fbbdf8a57c112e9f72096
combinators for local theories and lists

diff -r c2ce4797321a -r 7a24d827cba9 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Jul 11 12:23:44 2011 +0100
+++ b/Nominal/Nominal2.thy	Mon Jul 11 14:02:13 2011 +0200
@@ -215,27 +215,6 @@
 end
 *}
 
-ML {*
-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;
-(op ||>>)
-*}
-
-
 
 ML {*
 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
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