tuned;
authorwenzelm
Fri May 11 17:54:36 2007 +0200 (2007-05-11)
changeset 22936284b56463da8
parent 22935 c6689e15bc98
child 22937 08cf9aaf3aa1
tuned;
src/Pure/General/basics.ML
     1.1 --- a/src/Pure/General/basics.ML	Fri May 11 15:37:42 2007 +0200
     1.2 +++ b/src/Pure/General/basics.ML	Fri May 11 17:54:36 2007 +0200
     1.3 @@ -72,7 +72,8 @@
     1.4  fun `f = fn x => (f x, x);
     1.5  fun tap f = fn x => (f x; x);
     1.6  
     1.7 -fun flip f x y = f y x
     1.8 +fun flip f x y = f y x;
     1.9 +
    1.10  
    1.11  (* options *)
    1.12