src/Pure/term_sharing.ML
changeset 80738 6adf6cc82013
parent 79462 fbdffff89f99