op_mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list
Transforms a list into one with elements that are distinct modulo the supplied relation.
An invocation op_mk_set eq list returns a list consisting of the eq-distinct members of list. In particular, the result list will not contain elements x and y at different positions such that eq x y evaluates to true.
If an application of eq fails when applied to two elements of list.
- op_mk_set aconv [Term `\x y. x /\ y`,
                   Term `\y x. y /\ x`,
                   Term `\z a. z /\ a`];
> val it = [`\z a. z /\ a`] : term list

The order of items in the list returned by op_mk_set is not dependable.

A high-performance implementation of finite sets may be found in structure HOLset.

There is no requirement that eq be recognizable as a kind of equality (it could be implemented by an order relation, for example).

HOL  Kananaskis-14