dest_term : term -> lambda
STRUCTURE
Term
SYNOPSIS
Breaks terms into a type with SML constructors for pattern-matching.
DESCRIPTION
A call to dest_term t returns a value of type lambda, which has SML definition 
   datatype lambda =
      VAR of string * term
    | CONST of {Name:string, Thy:string, Ty:hol_type}
    | COMB of term * term
    | LAMB of term * term
This type encodes all possible forms of term.
FAILURE
Never fails.
EXAMPLE
> dest_term ``SUC 2``;
val it = COMB (``SUC``, ``2``) : lambda
SEEALSO
dest_abs, dest_comb, dest_const, dest_strip_comb, dest_thy_const, dest_var
HOL  Trindemossen-1