src/Pure/term_sharing.ML
changeset 80778 94bc8f62c835
parent 79462 fbdffff89f99