# HG changeset patch
# User wenzelm
# Date 880026565 -3600
# Node ID 5e8a31c41d440f4a8a724da28c359571e550133c
# Parent  9bba9251bb4d3308e84c995b4ccc1ddf5b7f684d
added get_error: 'a error -> string option, get_ok: 'a error -> 'a option;
added multiply: 'a list * 'a list list -> 'a list list;

diff -r 9bba9251bb4d -r 5e8a31c41d44 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 "";