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