src/Pure/deriv.ML
changeset 9234 0013b2aa98dd
parent 6085 3d8dcb09dbfb