--- a/src/Pure/library.ML Thu Sep 08 13:24:19 2005 +0200
+++ b/src/Pure/library.ML Thu Sep 08 16:08:50 2005 +0200
@@ -48,6 +48,8 @@
(*options*)
val the: 'a option -> 'a
val these: 'a list option -> 'a list
+ val the_default: 'a -> 'a option -> 'a
+ val the_list: 'a option -> 'a list
val if_none: 'a option -> 'a -> 'a
val is_some: 'a option -> bool
val is_none: 'a option -> bool
@@ -353,7 +355,11 @@
val the = Option.valOf;
fun these (SOME x) = x
- | these _ = []
+ | these _ = [];
+fun the_default x (SOME y) = y
+ | the_default x _ = x;
+fun the_list (SOME x) = [x]
+ | the_list _ = []
(*strict!*)
fun if_none NONE y = y