src/Pure/type.ML
changeset 13457 7ddcf40a80b3
parent 12726 5ae4034883d5
child 13666 a2730043029b