changeset 20821 | bae9a1002d84 |
parent 20297 | a9a917b356af |
child 20926 | b2f67b947200 |
--- a/src/Pure/context.ML Sun Oct 01 22:19:23 2006 +0200 +++ b/src/Pure/context.ML Sun Oct 01 22:19:24 2006 +0200 @@ -228,7 +228,8 @@ fun draft_id (_, name) = (name = draftN); val is_draft = draft_id o #id o identity_of; -fun exists_name name (Theory ({id, ids, iids, ...}, _, _, _)) = +fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) = + name = theory_name thy orelse name = #2 id orelse Inttab.exists (equal name o #2) ids orelse Inttab.exists (equal name o #2) iids;