src/Pure/type_infer.ML
changeset 14898 a25550451b51
parent 14854 61bdf2ae4dc5
child 14988 973ced82812d