src/HOL/Tools/functor.ML
changeset 82820 ae85cd17ffbe
parent 81513 d11ed1bf0ad2