src/Pure/term_subst.ML
changeset 80809 4a64fc4d1cde
parent 80607 e23aab2df03c