src/Pure/context.ML
changeset 26889 ccea41fb5c39
parent 26623 81547c8d51f8
child 26957 e3f04fdd994d
     1.1 --- a/src/Pure/context.ML	Wed May 14 14:43:34 2008 +0200
     1.2 +++ b/src/Pure/context.ML	Wed May 14 14:43:37 2008 +0200
     1.3 @@ -209,8 +209,8 @@
     1.4    Inttab.exists (equal name o #2) ids orelse
     1.5    Inttab.exists (equal name o #2) iids;
     1.6  
     1.7 -fun names_of (Theory ({id, ids, iids, ...}, _, _, _)) =
     1.8 -  rev (#2 id :: Inttab.fold (cons o #2) iids (Inttab.fold (cons o #2) ids []));
     1.9 +fun names_of (Theory ({id, ids, ...}, _, _, _)) =
    1.10 +  rev (#2 id :: Inttab.fold (cons o #2) ids []);
    1.11  
    1.12  fun pretty_thy thy =
    1.13    Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else []));