all_atoms : term -> term set
STRUCTURE
Term
SYNOPSIS
Returns variables and constants occurring in a term.
DESCRIPTION
A call to all_atoms t will return the set of all the variables and constants that appear in a term. The variables include those that occur under binders, even if only in binding position. Multiple instances of the same (polymorphic) constant can occur in the result if those instances are present in the term.

Because bound variables are returned as part of the result, alpha-equivalent terms will not necessarily give the same results when all_atoms is applied to them.

FAILURE
Never fails.
EXAMPLE
> HOLset.listItems (all_atoms ``!v. v /\ p``);
val it = [``p``, ``v``, ``$!``, ``$/\``]: term list

> show_types := true;
val it = () : unit

> HOLset.listItems (all_atoms ``!v. v /\ !f. f v``);
val it =
   [``(f :bool -> bool)``, ``(v :bool)``,
    ``($! :(bool -> bool) -> bool)``,
    ``($! :((bool -> bool) -> bool) -> bool)``,
    ``$/\``]: term list

> HOLset.listItems (all_atoms ``!v:'a. T``);
val it =
   [``(v :'a)``, ``($! :('a -> bool) -> bool)``, ``T``]: term list
COMMENTS
There is a companion function all_atomsl taking an accumulator, which has type term list -> term set -> term set.
SEEALSO
all_vars
HOL  Trindemossen-1