src/Pure/Tools/invoke.ML
changeset 22305 0e56750a092b
parent 22101 6d13239d5f52
child 22568 ed7aa5a350ef