src/Pure/type_infer.ML
changeset 21966 edab0ecfbd7c
parent 20854 f9cf9e62d11c
child 22678 23963361278c