src/Pure/Tools/invoke.ML
changeset 24711 e8bba7723858
parent 24693 fe88913f3706
child 24743 cfcdb9817c49