src/Pure/term_xml.ML
changeset 81656 7593c0976dc6
parent 80589 7849b6370425