added ` combinator
authorhaftmann
Thu Jul 14 10:48:19 2005 +0200 (2005-07-14)
changeset 168250a28f033de03
parent 16824 c889f499911c
child 16826 ed53f24149f6
added ` combinator
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Jul 14 10:32:01 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Jul 14 10:48:19 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 @@ -29,7 +29,7 @@
    1.13    val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    1.14    val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    1.15    val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
    1.16 -  val `> : 'b * ('b -> 'a) -> 'a * 'b
    1.17 +  val ` : ('b -> 'a) -> 'b -> 'a * 'b
    1.18    val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    1.19    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    1.20    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    1.21 @@ -310,7 +310,7 @@
    1.22  fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
    1.23  fun f #> g = g o f;
    1.24  fun f #-> g = fn s => let val (v, s') = f s in g v s' end;
    1.25 -fun x `> h = (h x, x)
    1.26 +fun ` h = fn s => (h s, s)
    1.27  
    1.28  (*composition with multiple args*)
    1.29  fun (f oo g) x y = f (g x y);