# 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 **)