added fun flip f x y = f y x
authorkrauss
Fri, 11 May 2007 15:37:42 +0200
changeset 22935 c6689e15bc98
parent 22934 64ecb3d6790a
child 22936 284b56463da8
added fun flip f x y = f y x
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 *)