Less broken define-fun declare-fun

This parses more of the declare-fun syntax correctly.