The constructor for declarations,  construct_declaration, takes
a pair of type  tok#term and produces a declaration.  The token
represents the variable name in the declaration.  The general destructor,
 destruct_declaration, maps a declaration into pair of type 
tok#term.  The ML
  function  
 id_of_declaration maps a declaration into
a token representing the variable of the declaration, and the function 
type_of_declaration maps a declaration to the term of the declaration.