src/Pure/type_infer.ML
changeset 20818 cb7ec413f95d
parent 20735 a041bf3c8f2f
child 20854 f9cf9e62d11c