# HG changeset patch
# User wenzelm
# Date 1254083113 -7200
# Node ID 9b014e62b716d22dccf80800473c0262f5b68575
# Parent  becd87e4039bf851004f42a9d9f50c0dcae4dff6# Parent  e24acd21e60e6d9193075f730626b41eebeee05d
merged

diff -r becd87e4039b -r 9b014e62b716 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sun Sep 27 19:58:24 2009 +0200
+++ b/src/Pure/General/graph.ML	Sun Sep 27 22:25:13 2009 +0200
@@ -132,21 +132,23 @@
   let
     fun reach x (rs, R) =
       if member_keys R x then (rs, R)
-      else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
-  in fold_map (fn x => fn X => reach x ([], X)) xs empty_keys end;
+      else fold reach (next x) (rs, insert_keys x R) |>> cons x;
+    fun reachs x (rss, R) =
+      reach x ([], R) |>> (fn rs => rs :: rss);
+  in fold reachs xs ([], empty_keys) end;
 
 (*immediate*)
 fun imm_preds G = #1 o #2 o get_entry G;
 fun imm_succs G = #2 o #2 o get_entry G;
 
 (*transitive*)
-fun all_preds G = flat o fst o reachable (imm_preds G);
-fun all_succs G = flat o fst o reachable (imm_succs G);
+fun all_preds G = flat o #1 o reachable (imm_preds G);
+fun all_succs G = flat o #1 o reachable (imm_succs G);
 
 (*strongly connected components; see: David King and John Launchbury,
   "Structuring Depth First Search Algorithms in Haskell"*)
-fun strong_conn G = filter_out null (fst (reachable (imm_preds G)
-  (flat (rev (fst (reachable (imm_succs G) (keys G)))))));
+fun strong_conn G =
+  rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
 
 
 (* nodes *)
diff -r becd87e4039b -r 9b014e62b716 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Sep 27 19:58:24 2009 +0200
+++ b/src/Pure/proofterm.ML	Sun Sep 27 22:25:13 2009 +0200
@@ -173,16 +173,19 @@
 
 fun fold_body_thms f =
   let
-    fun app (PBody {thms, ...}) =
+    fun app path (PBody {thms, ...}) =
      (Future.join_results (map (#3 o #2) thms);
       thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
-        if Inttab.defined seen i then (x, seen)
+        if Inttab.defined path i then
+          error ("Cyclic reference to theorem " ^ quote name)
+        else if Inttab.defined seen i then (x, seen)
         else
           let
             val body' = Future.join body;
-            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
+            val path' = Inttab.update (i, ()) path;
+            val (x', seen') = app path' body' (x, Inttab.update (i, ()) seen);
           in (f (name, prop, body') x', seen') end));
-  in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
+  in fn bodies => fn x => #1 (fold (app Inttab.empty) bodies (x, Inttab.empty)) end;
 
 fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();