dest_var : term -> string * hol_type
STRUCTURE
SYNOPSIS
Breaks apart a variable into name and type.
DESCRIPTION
If M is a HOL variable, then dest_var M returns (v,ty), where v is the name of the variable, an ty is its type.
FAILURE
Fails if M is not a variable.
SEEALSO
HOL  Trindemossen-1