src/Pure/Tools/codegen_names.ML
changeset 21404 eb85850d3eb7
parent 21338 56d55dd30311
child 21461 51239d45247b