| changeset 12311 | ce5f9e61c037 |
| parent 12123 | 739eba13e2cd |
| child 12378 | 86c58273f8c0 |
--- a/src/Pure/Isar/attrib.ML Wed Nov 28 00:44:37 2001 +0100 +++ b/src/Pure/Isar/attrib.ML Wed Nov 28 00:46:26 2001 +0100 @@ -56,7 +56,6 @@ 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}) =