# HG changeset patch
# User wenzelm
# Date 1119026010 -7200
# Node ID bc90e58bb6acc66e62789af80751e426662820e2
# Parent  80c8f742c6fc90ebd52d20f012e522c9a10767ff
Table.fold;

diff -r 80c8f742c6fc -r bc90e58bb6ac 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