same_const : term -> term -> bool
STRUCTURE
SYNOPSIS
Constant time equality check for constants.
DESCRIPTION
In many cases, one needs to check that a constant is an instance of the generic constant originally introduced into the signature, or that two constants are both type instantiations of another. This can be achieved by taking the constants apart with dest_thy_const and comparing their name and theory. However, this is relatively inefficient. Instead, one can invoke same_const, which takes constant time.
FAILURE
Never fails.
EXAMPLE
- same_const boolSyntax.universal (rator (concl BOOL_CASES_AX));

> val it = true : bool
SEEALSO
HOL  Kananaskis-13