fold_body_thms: pass pthm identifier;
fold_body_thms: dismiss path-etic attempt to check for cycles (cf. e24acd21e60e) -- could be masked by "seen";
fulfill_proof/thm_proof: check for thm cycles at the substitution point;

--- a/src/Pure/Thy/thm_deps.ML	Mon Sep 28 12:09:55 2009 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Mon Sep 28 20:52:05 2009 +0200
@@ -40,7 +40,7 @@
                path = "",
                parents = parents};
           in cons entry end;
-    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
+    val deps = Proofterm.fold_body_thms (add_dep o #2) (map Thm.proof_body_of thms) [];
   in Present.display_graph (sort_wrt #ID deps) end;
 
 
@@ -56,7 +56,7 @@
       |> sort_distinct (string_ord o pairself #1);
 
     val tab = Proofterm.fold_body_thms
-      (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
+      (fn (_, (name, prop, _)) => name <> "" ? Symtab.insert_list (op =) (name, prop))
       (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
     fun is_unused (name, th) =
       not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));

--- a/src/Pure/proofterm.ML	Mon Sep 28 12:09:55 2009 +0200
+++ b/src/Pure/proofterm.ML	Mon Sep 28 20:52:05 2009 +0200
@@ -40,7 +40,8 @@
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
-  val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
+  val fold_body_thms: (serial * (string * term * proof_body) -> 'a -> 'a) ->
+    proof_body list -> 'a -> 'a
   val join_bodies: proof_body list -> unit
   val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
@@ -109,7 +110,7 @@
   val axm_proof: string -> term -> proof
   val oracle_proof: string -> term -> oracle * proof
   val promise_proof: theory -> serial -> term -> proof
-  val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
+  val fulfill_proof: theory -> serial -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> term list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
   val get_name: term list -> term -> proof -> string
@@ -173,19 +174,16 @@
 
 fun fold_body_thms f =
   let
-    fun app path (PBody {thms, ...}) =
+    fun app (PBody {thms, ...}) =
      (Future.join_results (map (#3 o #2) thms);
       thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
-        if Inttab.defined path i then
-          error ("Cyclic reference to theorem " ^ quote name)
-        else if Inttab.defined seen i then (x, seen)
+        if Inttab.defined seen i then (x, seen)
         else
           let
             val body' = Future.join body;
-            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 Inttab.empty) bodies (x, Inttab.empty)) end;
+            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
+          in (f (i, (name, prop, body')) x', seen') end));
+  in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
 
 fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
 
@@ -1281,12 +1279,16 @@
         | _ => false));
   in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
 
-fun fulfill_proof _ [] body0 = body0
-  | fulfill_proof thy ps body0 =
+fun fulfill_proof _ _ [] body0 = body0
+  | fulfill_proof thy id ps body0 =
       let
         val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
-        val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
-        val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
+        val bodies = map snd ps;
+        val _ = fold_body_thms (fn (i, (name, _, _)) => fn () =>
+          if i = id then error ("Cyclic reference to theorem " ^ quote name)
+          else ()) bodies ();
+        val oracles = fold (fn PBody {oracles, ...} => merge_oracles oracles) bodies oracles0;
+        val thms = fold (fn PBody {thms, ...} => merge_thms thms) bodies thms0;
         val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
 
         fun fill (Promise (i, prop, Ts)) =
@@ -1298,10 +1300,10 @@
         val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
       in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
-fun fulfill_proof_future _ [] body = Future.value body
-  | fulfill_proof_future thy promises body =
+fun fulfill_proof_future _ _ [] body = Future.value body
+  | fulfill_proof_future thy id promises body =
       Future.fork_deps (map snd promises) (fn () =>
-        fulfill_proof thy (map (apsnd Future.join) promises) body);
+        fulfill_proof thy id (map (apsnd Future.join) promises) body);
 
 
 (***** theorems *****)
@@ -1321,7 +1323,9 @@
       else MinProof;
     val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
 
-    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
+    fun new_prf () =
+      let val id = serial ()
+      in (id, name, prop, fulfill_proof_future thy id promises body0) end;
     val (i, name, prop, body') =
       (case strip_combt (fst (strip_combP prf)) of
         (PThm (i, ((old_name, prop', NONE), body')), args') =>

--- a/src/Pure/thm.ML	Mon Sep 28 12:09:55 2009 +0200
+++ b/src/Pure/thm.ML	Mon Sep 28 20:52:05 2009 +0200
@@ -541,7 +541,7 @@
 fun raw_body (Thm (Deriv {body, ...}, _)) = body;
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
-  Pt.fulfill_proof (Theory.deref thy_ref)
+  Pt.fulfill_proof (Theory.deref thy_ref) ~1
     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
 and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));