src/Pure/Tools/invoke.ML
changeset 22264 6a65e9b2ae05
parent 22101 6d13239d5f52
child 22568 ed7aa5a350ef