exists_name: include this theory name;
authorwenzelm
Sun Oct 01 22:19:24 2006 +0200 (2006-10-01)
changeset 20821bae9a1002d84
parent 20820 58693343905f
child 20822 634070b40731
exists_name: include this theory name;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Sun Oct 01 22:19:23 2006 +0200
     1.2 +++ b/src/Pure/context.ML	Sun Oct 01 22:19:24 2006 +0200
     1.3 @@ -228,7 +228,8 @@
     1.4  fun draft_id (_, name) = (name = draftN);
     1.5  val is_draft = draft_id o #id o identity_of;
     1.6  
     1.7 -fun exists_name name (Theory ({id, ids, iids, ...}, _, _, _)) =
     1.8 +fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) =
     1.9 +  name = theory_name thy orelse
    1.10    name = #2 id orelse
    1.11    Inttab.exists (equal name o #2) ids orelse
    1.12    Inttab.exists (equal name o #2) iids;