# 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 *)