# HG changeset patch
# User wenzelm
# Date 1159733964 -7200
# Node ID bae9a1002d84c9a715e4a598233b2a88a2db07da
# Parent  58693343905f5295ac96fa2dcf69ca339641b6fe
exists_name: include this theory name;

diff -r 58693343905f -r bae9a1002d84 src/Pure/context.ML
--- 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;