src/Pure/codegen.ML
changeset 38810 361119ea62ee
parent 38329 16bb1e60204b
child 39253 0c47d615a69b
equal deleted inserted replaced
38809:7dc73a208722 38810:361119ea62ee