src/Pure/codegen.ML
changeset 40447 7434faac7e21
parent 40316 665862241968
child 40627 becf5d5187cc
equal deleted inserted replaced
40446:27c1a1c82eba 40447:7434faac7e21