We consider the problem of efficient term matching, modulo combinations of regular equational theories. Our general approach to the problem consists of three phases: compilation, matching and subproblem solving. We describe a technique for dealing with non-linear variables in a pattern and show how this technique is specialized to several specific equational theories. For matching in an order-sorted setting we discuss an important optimization for theories involving the associativity equation. Finally we sketch a new method of combining matching algorithms for regular collapse theories and give examples that involve the identity and idempotence equations.
(BibTeX entry) (gzip'ed Postscript)