src/Pure/term_sharing.ML
changeset 82874 abfb6ed8ec21
parent 79462 fbdffff89f99