----------------------------------------------------------------------
dest_const                                                      (Term)
----------------------------------------------------------------------
dest_const : term -> string * hol_type

SYNOPSIS
Breaks apart a constant into name and type.

DESCRIBE
{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
Term.mk_const, Term.mk_thy_const, Term.dest_thy_const, Term.is_const,
Term.dest_abs, Term.dest_comb, Term.dest_var.

----------------------------------------------------------------------