src/Pure/Tools/am_interpreter.ML
changeset 19215 03abed544f1e
parent 17795 5b18c3343028