# HG changeset patch # User wenzelm # Date 911212348 -3600 # Node ID c755dfd0250918c279cb07eda86c18e55dcb97b0 # Parent e5e44cc54eb2fc13f2d10b15587d0d5562de5446 added oo, ooo (*concatenation: 2 and 3 args*); diff -r e5e44cc54eb2 -r c755dfd02509 src/Pure/library.ML --- a/src/Pure/library.ML Mon Nov 16 11:14:44 1998 +0100 +++ b/src/Pure/library.ML Mon Nov 16 11:32:28 1998 +0100 @@ -12,6 +12,8 @@ mem mem_int mem_string union union_int union_string inter inter_int inter_string subset subset_int subset_string; +infix 3 oo ooo; + signature LIBRARY = sig (*functions*) @@ -23,6 +25,8 @@ val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c val funpow: int -> ('a -> 'a) -> 'a -> 'a + val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b + val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b (*stamps*) type stamp @@ -268,6 +272,9 @@ | rep (n, x) = rep (n - 1, f x) in rep (n, x) end; +(*concatenation: 2 and 3 args*) +fun (f oo g) x y = f (g x y); +fun (f ooo g) x y z = f (g x y z); (** stamps **)