src/Pure/library.ML
changeset 16688 e3de7ea24c23
parent 16676 671bd433b9eb
child 16691 539b9cc282fa
     1.1 --- a/src/Pure/library.ML	Tue Jul 05 13:55:09 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Jul 05 13:57:23 2005 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  tables, balanced trees, orders, current directory, misc.
     1.5  *)
     1.6  
     1.7 -infix |> |>> |>>> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
     1.8 +infix |> |-> |>> |>>> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
     1.9    mem mem_int mem_string union union_int union_string inter inter_int
    1.10    inter_string subset subset_int subset_string;
    1.11  
    1.12 @@ -22,6 +22,7 @@
    1.13    val I: 'a -> 'a
    1.14    val K: 'a -> 'b -> 'a
    1.15    val |> : 'a * ('a -> 'b) -> 'b
    1.16 +  val |-> : ('a * 'c) * ('c -> 'a -> 'b) -> 'b
    1.17    val |>> : ('a * 'b) * ('a -> 'c) -> 'c * 'b
    1.18    val |>>> : ('a * 'b) * ('a -> 'c * 'd) -> 'c * ('b * 'd)
    1.19    val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
    1.20 @@ -296,6 +297,7 @@
    1.21  
    1.22  (*reverse apply*)
    1.23  fun (x |> f) = f x;
    1.24 +fun ((x, v) |-> f) = f v x;
    1.25  fun ((x, y) |>> f) = (f x, y);
    1.26  fun ((x, y) |>>> f) = let val (x', z) = f x in (x', (y, z)) end;
    1.27