src/Pure/context.ML
changeset 20821 bae9a1002d84
parent 20297 a9a917b356af
child 20926 b2f67b947200
equal deleted inserted replaced
20820:58693343905f 20821:bae9a1002d84
   226 
   226 
   227 val draftN = "#";
   227 val draftN = "#";
   228 fun draft_id (_, name) = (name = draftN);
   228 fun draft_id (_, name) = (name = draftN);
   229 val is_draft = draft_id o #id o identity_of;
   229 val is_draft = draft_id o #id o identity_of;
   230 
   230 
   231 fun exists_name name (Theory ({id, ids, iids, ...}, _, _, _)) =
   231 fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) =
       
   232   name = theory_name thy orelse
   232   name = #2 id orelse
   233   name = #2 id orelse
   233   Inttab.exists (equal name o #2) ids orelse
   234   Inttab.exists (equal name o #2) ids orelse
   234   Inttab.exists (equal name o #2) iids;
   235   Inttab.exists (equal name o #2) iids;
   235 
   236 
   236 fun names_of (Theory ({id, ids, iids, ...}, _, _, _)) =
   237 fun names_of (Theory ({id, ids, iids, ...}, _, _, _)) =