src/Pure/General/basics.ML
changeset 23559 0de527730294
parent 23358 e0b5a74d7ace
child 28443 de653f1ad78b
equal deleted inserted replaced
23558:9325845aff1c 23559:0de527730294
    79 
    79 
    80 fun the (SOME x) = x
    80 fun the (SOME x) = x
    81   | the NONE = raise Option;
    81   | the NONE = raise Option;
    82 
    82 
    83 fun these (SOME x) = x
    83 fun these (SOME x) = x
    84   | these _ = [];
    84   | these NONE = [];
    85 
    85 
    86 fun the_list (SOME x) = [x]
    86 fun the_list (SOME x) = [x]
    87   | the_list _ = []
    87   | the_list NONE = []
    88 
    88 
    89 fun the_default x (SOME y) = y
    89 fun the_default x (SOME y) = y
    90   | the_default x _ = x;
    90   | the_default x NONE = x;
    91 
    91 
    92 fun perhaps f x = the_default x (f x);
    92 fun perhaps f x = the_default x (f x);
    93 
    93 
    94 
    94 
    95 (* partiality *)
    95 (* partiality *)