src/Pure/Thy/thy_element.ML
changeset 82689 817f97d8cd26
parent 82679 1dd29afaddda