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
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.