# HG changeset patch
# User wenzelm
# Date 1124356656 -7200
# Node ID 9c0aaa50283d5791034806f4a475988a79e32b78
# Parent  16d044ffad19d4100673e4117edc16f973c68f3c
added tap;

diff -r 16d044ffad19 -r 9c0aaa50283d src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Aug 18 11:17:35 2005 +0200
+++ b/src/Pure/library.ML	Thu Aug 18 11:17:36 2005 +0200
@@ -31,6 +31,7 @@
   val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
   val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
   val ` : ('b -> 'a) -> 'b -> 'a * 'b
+  val tap: ('b -> 'a) -> 'b -> 'b
   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
@@ -321,6 +322,7 @@
 
 (*view results*)
 fun `f = fn x => (f x, x);
+fun tap f x = (f x; x);
 
 (*composition with multiple args*)
 fun (f oo g) x y = f (g x y);