equal
deleted
inserted
replaced
54 ((((Args.src -> theory attribute) * (Args.src -> Proof.context attribute)) |
54 ((((Args.src -> theory attribute) * (Args.src -> Proof.context attribute)) |
55 * string) * stamp) Symtab.table}; |
55 * string) * stamp) Symtab.table}; |
56 |
56 |
57 val empty = {space = NameSpace.empty, attrs = Symtab.empty}; |
57 val empty = {space = NameSpace.empty, attrs = Symtab.empty}; |
58 val copy = I; |
58 val copy = I; |
59 val finish = I; |
|
60 val prep_ext = I; |
59 val prep_ext = I; |
61 |
60 |
62 fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) = |
61 fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) = |
63 {space = NameSpace.merge (space1, space2), |
62 {space = NameSpace.merge (space1, space2), |
64 attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups => |
63 attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups => |