tuned;

--- a/src/Pure/library.ML	Thu Dec 08 20:16:10 2005 +0100
+++ b/src/Pure/library.ML	Thu Dec 08 20:16:17 2005 +0100
@@ -341,10 +341,8 @@
 fun is_none (SOME _) = false
   | is_none NONE = true;
 
-fun perhaps f x =
-  case f x
-   of NONE => x
-    | SOME x' => x';
+fun perhaps f x = the_default x (f x);
+
 
 (* exceptions *)