src/Pure/library.ML

--- a/src/Pure/library.ML	Thu Nov 20 12:48:00 1997 +0100
+++ b/src/Pure/library.ML	Thu Nov 20 12:49:25 1997 +0100
@@ -258,6 +258,10 @@
     else rep (n, [])
   end;
 
+(*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
+fun multiply ([], _) = []
+  | multiply (x :: xs, yss) = map (cons x) yss @ multiply (xs, yss);
+
 
 (* filter *)
 
@@ -782,6 +786,12 @@
   Error of string |
   OK of 'a;
 
+fun get_error (Error msg) = Some msg
+  | get_error _ = None;
+
+fun get_ok (OK x) = Some x
+  | get_ok _ = None;
+
 fun handle_error f x =
   let
     val buffer = ref "";