dest_thy_const : term -> {Thy:string, Name:string, Ty:hol_type}
STRUCTURE
Term
SYNOPSIS
Breaks apart a constant into name, theory, and type.
DESCRIPTION
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
mk_const, dest_thy_const, is_const, dest_abs, dest_comb, dest_var
HOL  Kananaskis-10