diff -r 159783c74f75 -r 7d97f60293ae src/Pure/library.ML
--- 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