src/Pure/Tools/codegen_names.ML
changeset 22264 6a65e9b2ae05
parent 22197 461130ccfef4
child 22304 ba3d6b76a627