src/Pure/term_subst.ML
changeset 80264 71c1cf9e7413
parent 79409 e1895596e1b9
child 80599 f8c070249502