src/Pure/General/basics.ML
changeset 22935 c6689e15bc98
parent 21394 9f20604d2b5e
child 22936 284b56463da8
--- 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 *)