changeset 18376 | 2ef0183fa20b |
parent 18359 | 02a830bab542 |
child 18427 | b7ee916ae3ec |
--- 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 *)