src/Pure/unify.ML
changeset 79818 0c2a62a9f136
parent 79743 3648e9c88d0c
child 80328 559909bd7715