src/Pure/ML-Systems/exn.ML

export just one setup function;
more antiquotations;
to_nnf: import open, avoiding internal variables (bounds);
ThmCache: added table of seen fact names;
reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end;
removed obsolete skolem attribute (NB: official fact name unavailable here);

(*  Title:      Pure/ML-Systems/exn.ML
    ID:         $Id$
    Author:     Makarius

Runtime exceptions as values.
*)

structure Exn =
struct

datatype 'a result =
  Result of 'a |
  Exn of exn;

fun get_result (Result x) = SOME x
  | get_result _ = NONE;

fun get_exn (Exn exn) = SOME exn
  | get_exn _ = NONE;

fun capture f x = Result (f x) handle e => Exn e;

fun release (Result y) = y
  | release (Exn e) = raise e;

exception EXCEPTIONS of exn list * string;

end;