src/Pure/type.ML
changeset 33930 6a973bd43949
parent 33832 cff42395c246
child 33941 40408e6b833b