src/Pure/type_infer.ML
changeset 5526 e7617b57a3e6
parent 4957 30c49821e61f
child 5634 7f61a83d4a01