tuned;
authorwenzelm
Thu Dec 08 20:16:17 2005 +0100 (2005-12-08)
changeset 183762ef0183fa20b
parent 18375 99deeed095ae
child 18377 0e1d025d57b3
tuned;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Dec 08 20:16:10 2005 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Dec 08 20:16:17 2005 +0100
     1.3 @@ -341,10 +341,8 @@
     1.4  fun is_none (SOME _) = false
     1.5    | is_none NONE = true;
     1.6  
     1.7 -fun perhaps f x =
     1.8 -  case f x
     1.9 -   of NONE => x
    1.10 -    | SOME x' => x';
    1.11 +fun perhaps f x = the_default x (f x);
    1.12 +
    1.13  
    1.14  (* exceptions *)
    1.15