# HG changeset patch
# User wenzelm
# Date 1192122621 -7200
# Node ID 783bf93c8f920950a9391eda24415fd0202960c9
# Parent  159b0f4dd1e969cb6aed334a684ef32917d6ca41
removed obsolete flip;

diff -r 159b0f4dd1e9 -r 783bf93c8f92 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Oct 11 19:10:20 2007 +0200
+++ b/src/Pure/library.ML	Thu Oct 11 19:10:21 2007 +0200
@@ -22,7 +22,6 @@
   val undefined: 'a -> 'b
   val I: 'a -> 'a
   val K: 'a -> 'b -> 'a
-  val flip: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
   val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
   val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
   val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
@@ -244,7 +243,6 @@
 
 fun I x = x;
 fun K x = fn _ => x;
-fun flip f x y = f y x;
 fun curry f x y = f (x, y);
 fun uncurry f (x, y) = f x y;