Term.dest

dest_var : term -> string * hol_type

STRUCTURE: Term
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: mk_var, is_var, dest_const, dest_comb, dest_abs

HOL Kananaskis-13