src/Pure/Tools/am_interpreter.ML
changeset 20988 0887d0dd3210
parent 17795 5b18c3343028