# HG changeset patch
# User wenzelm
# Date 1178898876 -7200
# Node ID 284b56463da8d14f40456902122afef423c498fc
# Parent  c6689e15bc98ac439d9d7ba4ecc52429f0799a48
tuned;

diff -r c6689e15bc98 -r 284b56463da8 src/Pure/General/basics.ML
--- a/src/Pure/General/basics.ML	Fri May 11 15:37:42 2007 +0200
+++ b/src/Pure/General/basics.ML	Fri May 11 17:54:36 2007 +0200
@@ -72,7 +72,8 @@
 fun `f = fn x => (f x, x);
 fun tap f = fn x => (f x; x);
 
-fun flip f x y = f y x
+fun flip f x y = f y x;
+
 
 (* options *)