changeset 12311 | ce5f9e61c037 |
parent 12123 | 739eba13e2cd |
child 12452 | 68493b92e7a6 |
--- a/src/Pure/codegen.ML Wed Nov 28 00:44:37 2001 +0100 +++ b/src/Pure/codegen.ML Wed Nov 28 00:46:26 2001 +0100 @@ -82,7 +82,6 @@ val empty = {codegens = [], consts = [], types = []}; val copy = I; - val finish = I; val prep_ext = I; fun merge ({codegens = codegens1, consts = consts1, types = types1},