src/HOL/Subst/Unifier.ML
changeset 14352 a8b1a44d8264
parent 5278 a903b66822e2