src/Pure/term_sharing.ML
changeset 79873 6c19c29ddcbe
parent 79462 fbdffff89f99