| changeset 12123 | 739eba13e2cd |
| parent 11904 | 3a4b3c311a97 |
| child 12311 | ce5f9e61c037 |
--- a/src/Pure/Isar/attrib.ML Fri Nov 09 00:18:23 2001 +0100 +++ b/src/Pure/Isar/attrib.ML Fri Nov 09 00:19:20 2001 +0100 @@ -56,6 +56,7 @@ val empty = {space = NameSpace.empty, attrs = Symtab.empty}; val copy = I; + val finish = I; val prep_ext = I; fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) =