src/Pure/type_infer.ML
changeset 6942 f291292d727c
parent 5635 b7d6b7f66131
child 7639 538bd31709cb