| changeset 12123 | 739eba13e2cd |
| parent 11546 | 2b3f02227c35 |
| child 12311 | ce5f9e61c037 |
--- a/src/Pure/codegen.ML Fri Nov 09 00:18:23 2001 +0100 +++ b/src/Pure/codegen.ML Fri Nov 09 00:19:20 2001 +0100 @@ -82,6 +82,7 @@ val empty = {codegens = [], consts = [], types = []}; val copy = I; + val finish = I; val prep_ext = I; fun merge ({codegens = codegens1, consts = consts1, types = types1},