Safety verification problems are often reduced to solving the satisfiability of Constrained Horn Clauses (CHCs), a set of constraints in first-order logic involving uninterpreted predicates. Synthesis of interpretations for the predicates, also known as inductive invariants synthesis, is challenging in the presence of Algebraic Data Types (ADTs). Defined inductively, ADTs describe possibly unbounded chunks of data, thus they often require synthesizing recursive invariants. We present a novel approach to this problem based on functional synthesis: it attempts to extract recursive functions from constraints that capture the semantics of unbounded computation over the chunks of data encoded in CHCs. Recursive function calls are beneficial since they allow rewriting the constraints and introducing equalities that further can be simplified away. This largely simplifies the problem of generating invariants and lets them have simple interpretations that are recursion-free at the highest level and have function calls. We have implemented the approach in a new CHC solver called AdtChc. Our algorithm relies on an external automated theorem prover to conduct proofs by structural induction, as opposed to a black-box constrained solver. With two alternative solvers of choice, AdtInd and Vampire, the new toolset has been evaluated on a range of public benchmarks, and it exhibited its strengths against state-of-the-art CHC solvers on particular benchmarks that require recursive invariants.