src/Pure/Tools/legacy_xml_syntax.ML
changeset 52432 c03090937c3b
parent 50217 ce1f0602f48e