src/HOL/Subst/Unify.ML
changeset 9738 2e1dca5af2d4
parent 9736 332fab43628f
child 10768 a7282df327c6