genvarstruct : hol_type -> term
STRUCTURE
LIBRARY
pair
SYNOPSIS
Returns a pair structure of variables whose names have not been previously used.
DESCRIPTION
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
HOL  Kananaskis-13