src/Pure/unify.ML
changeset 3257 4e3724e0659f
parent 2753 bcde71e5f371
child 3991 4cb2f2422695