src/Pure/term_subst.ML
changeset 69510 0f31dd2e540d
parent 69023 cef000855cf4
child 74200 17090e27aae9