exists_name: include this theory name;
authorwenzelm
Sun, 01 Oct 2006 22:19:24 +0200
changeset 20821 bae9a1002d84
parent 20820 58693343905f
child 20822 634070b40731
exists_name: include this theory name;
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;