----------------------------------------------------------------------
genvar                                                          (Term)
----------------------------------------------------------------------
genvar : hol_type -> term

SYNOPSIS
Returns a variable whose name has not been used previously.

DESCRIBE
When given a type, {genvar} returns a variable of that type whose name has
not been used for a variable or constant in the HOL session so far.

FAILURE
Never fails.

EXAMPLE
The following indicates the typical stylized form of the names (this should
not be relied on, of course):

   - genvar bool;
   > val it = `%%genvar%%1380` : term

   - genvar (Type`:num`);
   > val it = `%%genvar%%1381` : term

Note that one can anticipate {genvar}:

   - mk_var("%%genvar%%1382",bool);
   > val it = `%%genvar%%1382` : term

   - genvar bool;
   > val it = `%%genvar%%1382` : term


This shortcoming could be guarded against, but it doesn’t seem worth
it currently. It doesn’t seem to affect the soundness of the
implementation of HOL; at worst, a proof procedure may fail because
it doesn’t have a sufficiently fresh variable.

USES
The unique variables are useful in writing derived rules, for specializing
terms without having to worry about such things as free variable capture.
If the names are to be visible to a typical user, the function {variant} can
provide rather more meaningful names.

SEEALSO
Drule.GSPEC, Term.variant.

----------------------------------------------------------------------