names_of: exclude intermediate ids -- less verbosity;
authorwenzelm
Wed May 14 14:43:37 2008 +0200 (2008-05-14)
changeset 26889ccea41fb5c39
parent 26888 9942cd184c48
child 26890 f9ec18f7c0f6
names_of: exclude intermediate ids -- less verbosity;
src/Pure/context.ML
     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 []));