src/Pure/unify.ML
changeset 80264 71c1cf9e7413
parent 79743 3648e9c88d0c
child 80328 559909bd7715