----------------------------------------------------------------------
genvarstruct                                              (pairSyntax)
----------------------------------------------------------------------
genvarstruct : hol_type -> term

LIBRARY
pair

SYNOPSIS
Returns a pair structure of variables whose names have not been previously used.

DESCRIBE
When given a product type, {genvarstruct} returns a
paired structure of variables whose names have not been
used for variables or constants in the HOL session so far.
The structure of the term returned will be identical to the structure of the
argument.

FAILURE
Never fails.

EXAMPLE
The following example illustrates the behaviour of {genvarstruct}:

   - genvarstruct (type_of (Term `((1,2),(x:'a,x:'a))`));
   > val it = `((%%genvar%%1535,%%genvar%%1536),%%genvar%%1537,%%genvar%%1538)`
      : term




USES
Unique variables are useful in writing derived rules, for specializing
terms without having to worry about such things as free variable capture.
It is often important in such rules to keep the same structure.
If not, {genvar} will be adequate.
If the names are to be visible to a typical user, the function {pvariant} can
provide rather more meaningful names.

SEEALSO
Term.genvar, PairRules.GPSPEC, pairSyntax.pvariant.

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