src/Pure/library.ML
changeset 4248 5e8a31c41d44
parent 4224 79e205c3a82c
child 4255 63ab0616900b
--- 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 "";