src/Pure/type_infer.ML
changeset 7714 e6aa4fca983e
parent 7639 538bd31709cb
child 8087 4187ef29d826