src/Pure/Tools/am_util.ML
changeset 17349 03fafcdfdfa7
parent 16842 5979c46853d1
child 17799 1cc6e60bd5ff