diff -r e883d1332662 -r b356f7837921 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Dec 02 16:04:29 2005 +0100
+++ b/src/Pure/library.ML	Fri Dec 02 16:04:48 2005 +0100
@@ -51,6 +51,7 @@
   val if_none: 'a option -> 'a -> 'a
   val is_some: 'a option -> bool
   val is_none: 'a option -> bool
+  val perhaps: ('a -> 'a option) -> 'a -> 'a
 
   exception EXCEPTION of exn * string
   exception ERROR
@@ -339,6 +340,10 @@
 fun is_none (SOME _) = false
   | is_none NONE = true;
 
+fun perhaps f x =
+  case f x
+   of NONE => x
+    | SOME x' => x';
 
 (* exceptions *)