We present a new formalization in the Isabelle proof assistant of first-order syntactic unification, including a proof of termination. Our formalization follows, almost down to the letter, the ML-code from Baader and Nipkow's book "Term Rewriting and All That" (1998). Correctness is implied by the formalization's similarity to Baader and Nipkow's ML-code, but we have yet to formalize the correctness of the unification algorithm.
Paper accepted at International Workshop on Unification (UNIF 2018) http://unif2018.cic.unb.br/
Use Isabelle2018 https://sketis.net/2018/release-candidates-for-isabelle2018