# HG changeset patch
# User wenzelm
# Date 925202528 -7200
# Node ID b5ef6d115b45696b3e3b1a6bab8c9b19a4d7264b
# Parent  9f7f4fd05b1fb4820c8919d6ce512d9015e7c74f
added oooo;

diff -r 9f7f4fd05b1f -r b5ef6d115b45 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Apr 26 13:25:49 1999 +0200
+++ b/src/Pure/library.ML	Tue Apr 27 10:42:08 1999 +0200
@@ -12,7 +12,7 @@
   mem mem_int mem_string union union_int union_string inter inter_int
   inter_string subset subset_int subset_string;
 
-infix 3 oo ooo;
+infix 3 oo ooo oooo;
 
 signature LIBRARY =
 sig
@@ -27,6 +27,7 @@
   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
+  val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
 
   (*stamps*)
   type stamp
@@ -281,6 +282,8 @@
 (*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);
+fun (f oooo g) x y z w = f (g x y z w);
+
 
 
 (** stamps **)