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.