src/Pure/deriv.ML
changeset 7022 abf9d5e2fb6e
parent 6085 3d8dcb09dbfb