diff -r 7bbd3751523f -r 3f38cbd57d47 src/Pure/basis.ML
--- a/src/Pure/basis.ML	Wed Apr 02 11:30:48 1997 +0200
+++ b/src/Pure/basis.ML	Wed Apr 02 11:32:48 1997 +0200
@@ -18,6 +18,23 @@
     | toString false = "false"
   end;
 
+structure General =
+  struct
+  exception Option
+
+  datatype 'a option = NONE | SOME of 'a
+
+  fun getOpt (SOME v, _) = v
+    | getOpt (NONE,   a) = a
+
+  fun isSome (SOME _) = true 
+    | isSome NONE     = false
+
+  fun valOf (SOME v) = v
+    | valOf NONE     = raise Option
+  end;
+
+
 structure Int =
   struct
   fun toString (i: int) = makestring i;
@@ -53,6 +70,11 @@
 
   fun concat []      = []
     | concat (l::ls) = l @ concat ls;
+
+  fun mapPartial f []      = []
+    | mapPartial f (x::xs) = 
+         (case f x of General.NONE   => mapPartial f xs
+                    | General.SOME y => y :: mapPartial f xs);
   end;