added get_error: 'a error -> string option, get_ok: 'a error -> 'a option;
authorwenzelm
Thu Nov 20 12:49:25 1997 +0100 (1997-11-20)
changeset 42485e8a31c41d44
parent 4247 9bba9251bb4d
child 4249 34b7aafdc1bc
added get_error: 'a error -> string option, get_ok: 'a error -> 'a option;
added multiply: 'a list * 'a list list -> 'a list list;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Nov 20 12:48:00 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Nov 20 12:49:25 1997 +0100
     1.3 @@ -258,6 +258,10 @@
     1.4      else rep (n, [])
     1.5    end;
     1.6  
     1.7 +(*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
     1.8 +fun multiply ([], _) = []
     1.9 +  | multiply (x :: xs, yss) = map (cons x) yss @ multiply (xs, yss);
    1.10 +
    1.11  
    1.12  (* filter *)
    1.13  
    1.14 @@ -782,6 +786,12 @@
    1.15    Error of string |
    1.16    OK of 'a;
    1.17  
    1.18 +fun get_error (Error msg) = Some msg
    1.19 +  | get_error _ = None;
    1.20 +
    1.21 +fun get_ok (OK x) = Some x
    1.22 +  | get_ok _ = None;
    1.23 +
    1.24  fun handle_error f x =
    1.25    let
    1.26      val buffer = ref "";