diff -r a78e5d399599 -r 09bf3b73e446 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Thu Jul 19 14:24:40 2012 +0200
+++ b/src/Pure/General/graph.ML	Thu Jul 19 15:45:59 2012 +0200
@@ -144,7 +144,7 @@
   let
     fun reach x (rs, R) =
       if Keys.member R x then (rs, R)
-      else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
+      else Keys.fold_rev reach (next x) (rs, Keys.insert x R) |>> cons x;
     fun reachs x (rss, R) =
       reach x ([], R) |>> (fn rs => rs :: rss);
   in fold reachs xs ([], Keys.empty) end;