dest_const : term -> string * hol_type
Breaks apart a constant into name and type.
dest_const is a term destructor for constants. If M is a
constant with name c and type ty, then dest_const M
Fails if M is not a constant.
In Hol98, constants also carry the theory they are declared in. A
more precise and robust way to analyze a constant is with