src/Pure/term_subst.ML
changeset 28815 80bb72a0f577
parent 21607 3698319f6503
child 29269 5c25a2012975