Table.fold;
authorwenzelm
Fri Jun 17 18:33:30 2005 +0200 (2005-06-17)
changeset 16445bc90e58bb6ac
parent 16444 80c8f742c6fc
child 16446 0ab34b9d1b1f
Table.fold;
src/Pure/General/graph.ML
     1.1 --- a/src/Pure/General/graph.ML	Fri Jun 17 18:33:29 2005 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Fri Jun 17 18:33:30 2005 +0200
     1.3 @@ -81,10 +81,8 @@
     1.4  fun keys (Graph tab) = Table.keys tab;
     1.5  fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
     1.6  
     1.7 -fun minimals (Graph tab) =
     1.8 -  Table.foldl (fn (ms, (m, (_, ([], _)))) => m :: ms | (ms, _) => ms) ([], tab);
     1.9 -fun maximals (Graph tab) =
    1.10 -  Table.foldl (fn (ms, (m, (_, (_, [])))) => m :: ms | (ms, _) => ms) ([], tab);
    1.11 +fun minimals (Graph tab) = Table.fold (fn (m, (_, ([], _))) => cons m | _ => I) tab [];
    1.12 +fun maximals (Graph tab) = Table.fold (fn (m, (_, (_, []))) => cons m | _ => I) tab [];
    1.13  
    1.14  fun get_entry (Graph tab) x =
    1.15    (case Table.lookup (tab, x) of