src/Pure/context.ML
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;