src/Pure/term_sharing.ML
changeset 80264 71c1cf9e7413
parent 79462 fbdffff89f99