dest_const : term -> string * hol_type
STRUCTURE
SYNOPSIS
Breaks apart a constant into name and type.
DESCRIPTION
dest_const is a term destructor for constants. If M is a constant with name c and type ty, then dest_const M returns (c,ty).
FAILURE
Fails if M is not a constant.
COMMENTS
In Hol98, constants also carry the theory they are declared in. A more precise and robust way to analyze a constant is with dest_thy_const.
SEEALSO
HOL  Trindemossen-1