# HG changeset patch
# User krauss
# Date 1178890662 -7200
# Node ID c6689e15bc98ac439d9d7ba4ecc52429f0799a48
# Parent  64ecb3d6790adee759bb30b9ca244e58b4f40e3a
added fun flip f x y = f y x

diff -r 64ecb3d6790a -r c6689e15bc98 src/Pure/General/basics.ML
--- a/src/Pure/General/basics.ML	Fri May 11 03:31:12 2007 +0200
+++ b/src/Pure/General/basics.ML	Fri May 11 15:37:42 2007 +0200
@@ -23,6 +23,7 @@
   val ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd
   val ` : ('b -> 'a) -> 'b -> 'a * 'b
   val tap: ('b -> 'a) -> 'b -> 'b
+  val flip: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
 
   (*options*)
   val is_some: 'a option -> bool
@@ -71,6 +72,7 @@
 fun `f = fn x => (f x, x);
 fun tap f = fn x => (f x; x);
 
+fun flip f x y = f y x
 
 (* options *)