src/Pure/sorts.ML
changeset 81656 7593c0976dc6
parent 79447 57d29f537723