src/Pure/type_infer.ML
changeset 5867 1c4806b4bf43
parent 5635 b7d6b7f66131
child 7639 538bd31709cb