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