We present a procedure for the bounded unification of higher-order terms [22]. The procedure extends G. P. Huet’s pre-unification procedure [11] with rules for the generation and folding of regular terms. The concise form of the procedure allows the reuse of the pre- unification correctness proof. Furthermore, the regular terms can be restricted in order to decide the unifiability problem. Finally, the procedure avoids re-computation of terms in a non-deterministic search which leads to a better performance in practice when compared to other bounded unification algorithms.