# HG changeset patch
# User haftmann
# Date 1120564643 -7200
# Node ID e3de7ea24c237a5f1bd35d108a7f2a11dac69117
# Parent  51fa05ce0f3213a852205f76a3ddab5dfb5851ff
added ST combinator '|->'

diff -r 51fa05ce0f32 -r e3de7ea24c23 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jul 05 13:55:09 2005 +0200
+++ b/src/Pure/library.ML	Tue Jul 05 13:57:23 2005 +0200
@@ -8,7 +8,7 @@
 tables, balanced trees, orders, current directory, misc.
 *)
 
-infix |> |>> |>>> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
+infix |> |-> |>> |>>> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
   mem mem_int mem_string union union_int union_string inter inter_int
   inter_string subset subset_int subset_string;
 
@@ -22,6 +22,7 @@
   val I: 'a -> 'a
   val K: 'a -> 'b -> 'a
   val |> : 'a * ('a -> 'b) -> 'b
+  val |-> : ('a * 'c) * ('c -> 'a -> 'b) -> 'b
   val |>> : ('a * 'b) * ('a -> 'c) -> 'c * 'b
   val |>>> : ('a * 'b) * ('a -> 'c * 'd) -> 'c * ('b * 'd)
   val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
@@ -296,6 +297,7 @@
 
 (*reverse apply*)
 fun (x |> f) = f x;
+fun ((x, v) |-> f) = f v x;
 fun ((x, y) |>> f) = (f x, y);
 fun ((x, y) |>>> f) = let val (x', z) = f x in (x', (y, z)) end;