src/HOL/Tools/functor.ML
changeset 80946 b76f64d7d493
parent 80634 a90ab1ea6458
child 81513 d11ed1bf0ad2