src/Pure/type_infer.ML
changeset 9218 fdecb23119c0
parent 8611 49166d549426
child 13629 a46362d2b19b