src/Pure/type_infer.ML
changeset 5526 e7617b57a3e6
parent 4957 30c49821e61f
child 5634 7f61a83d4a01
equal deleted inserted replaced
5525:896f8234b864 5526:e7617b57a3e6