# HG changeset patch
# User wenzelm
# Date 1134069377 -3600
# Node ID 2ef0183fa20b55886e4a50012b4441b285c7c4e4
# Parent  99deeed095aed1bf8dc5075293dccd2b6fd481f1
tuned;

diff -r 99deeed095ae -r 2ef0183fa20b src/Pure/library.ML
--- 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 *)