genvar : hol_type -> term
Returns a variable whose name has not been used previously.
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.
Never fails.
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.

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.
HOL  Kananaskis-14