----------------------------------------------------------------------
dest_thy_const                                                  (Term)
----------------------------------------------------------------------
dest_thy_const : term -> {Thy:string, Name:string, Ty:hol_type}

SYNOPSIS
Breaks apart a constant into name, theory, and type.

DESCRIBE
{dest_thy_const} is a term destructor for constants. If {M} is a
constant, declared in theory {Thy} with name {Name}, having type {ty},
then {dest_thy_const M} returns {{Thy, Name, Ty}}, where {Ty} is equal
to {ty}.

FAILURE
Fails if {M} is not a constant.

COMMENTS
A more precise alternative to {dest_const}.

SEEALSO
Term.mk_const, Term.dest_thy_const, Term.is_const, Term.dest_abs,
Term.dest_comb, Term.dest_var.

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