author | wenzelm |
Sun, 01 Oct 2006 22:19:24 +0200 | |
changeset 20821 | bae9a1002d84 |
parent 20820 | 58693343905f |
child 20822 | 634070b40731 |
--- 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;