mk_var : string * hol_type -> term
STRUCTURE
SYNOPSIS
Constructs a variable of given name and type.
DESCRIPTION
If v is a string and ty is a HOL type, then mk_var(v, ty) returns a HOL variable.
FAILURE
Never fails.
COMMENTS
mk_var can be used to construct variables with names which are not acceptable to the term parser. In particular, a variable with the name of a known constant can be constructed using mk_var.
SEEALSO
HOL  Trindemossen-1