src/Pure/deriv.ML
changeset 6942 f291292d727c
parent 6085 3d8dcb09dbfb