On Wed, 19 Dec 2007, George Karabotsos wrote:

Isabelle has the following definition under HOL:

consts the :: "'a option => 'a" primrec "the (Some x) = x"

I am wondering if there is anything equivalent in ML?

The Isabelle ML environment defines the following basic operations on options:

fun is_some (SOME _) = true | is_some NONE = false;

fun is_none (SOME _) = false | is_none NONE = true;

fun the (SOME x) = x | the NONE = raise Option;

fun these (SOME x) = x | these NONE = [];

fun the_list (SOME x) = [x] | the_list NONE = []

fun the_default x (SOME y) = y | the_default x NONE = x;

fun perhaps f x = the_default x (f x);

The New Jersey library defines other versions (cf. structure Option), but we rarely use it (apart from Option.map), because its conventions do not really fit into the general Isabelle framework.

Makarius