1.1 --- a/src/Pure/library.ML	Tue Jul 12 18:44:32 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Jul 12 19:18:55 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 @@ -23,10 +23,13 @@
    1.13    val K: 'a -> 'b -> 'a
    1.14    val |> : 'a * ('a -> 'b) -> 'b
    1.15    val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
    1.16 +  val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
    1.17 +  val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
    1.18    val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c
    1.19 -  val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
    1.20    val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    1.21 -  val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
    1.22 +  val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    1.23 +  val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
    1.24 +  val `> : 'b * ('b -> 'a) -> 'a * 'b
    1.25    val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    1.26    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    1.27    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    1.28 @@ -87,7 +90,7 @@
    1.29    val apply: ('a -> 'a) list -> 'a -> 'a
    1.30    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.31    val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.32 -  val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    1.33 +  val fold_yield: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    1.34    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.35    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.36    val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.37 @@ -305,6 +308,9 @@
    1.38  fun (x, y) ||> f = (x, f y);
    1.39  fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
    1.40  fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
    1.41 +fun f #> g = g o f;
    1.42 +fun f #-> g = fn s => let val (v, s') = f s in g v s' end;
    1.43 +fun x `> h = (h x, x)
    1.44  
    1.45  (*composition with multiple args*)
    1.46  fun (f oo g) x y = f (g x y);
    1.47 @@ -470,7 +476,7 @@
    1.48        | fold_aux (x :: xs) y = f x (fold_aux xs y);
    1.49    in fold_aux end;
    1.50  
    1.51 -fun fold_map f =
    1.52 +fun fold_yield f =
    1.53    let
    1.54      fun fold_aux [] y = ([], y)
    1.55        | fold_aux (x :: xs) y =