back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;

--- a/src/Pure/Thy/thm_deps.ML	Thu Oct 01 14:11:28 2009 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Thu Oct 01 14:27:50 2009 +0200
@@ -40,7 +40,7 @@
                path = "",
                parents = parents};
           in cons entry end;
-    val deps = Proofterm.fold_body_thms (add_dep o #2) (map Thm.proof_body_of thms) [];
+    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
   in Present.display_graph (sort_wrt #ID deps) end;
 
 
@@ -55,9 +55,10 @@
       fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
       |> sort_distinct (string_ord o pairself #1);
 
-    val tab = Proofterm.fold_body_thms
-      (fn (_, (name, prop, _)) => name <> "" ? Symtab.insert_list (op =) (name, prop))
-      (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
+    val tab =
+      Proofterm.fold_body_thms
+        (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	Thu Oct 01 14:11:28 2009 +0200
+++ b/src/Pure/proofterm.ML	Thu Oct 01 14:27:50 2009 +0200
@@ -40,8 +40,7 @@
   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: (serial * (string * term * proof_body) -> 'a -> 'a) ->
-    proof_body list -> 'a -> 'a
+  val fold_body_thms: (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}
 
@@ -110,7 +109,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 -> (serial * proof_body) list -> proof_body -> proof_body
+  val fulfill_proof: theory -> (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
@@ -182,7 +181,7 @@
           let
             val body' = Future.join body;
             val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
-          in (f (i, (name, prop, body')) x', seen') end));
+          in (f (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 ();
@@ -1279,16 +1278,12 @@
         | _ => false));
   in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
 
-fun fulfill_proof _ _ [] body0 = body0
-  | fulfill_proof thy id ps body0 =
+fun fulfill_proof _ [] body0 = body0
+  | fulfill_proof thy ps body0 =
       let
         val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
-        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 oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
+        val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
         val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
 
         fun fill (Promise (i, prop, Ts)) =
@@ -1300,18 +1295,18 @@
         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 id promises body =
+fun fulfill_proof_future _ [] body = Future.value body
+  | fulfill_proof_future thy promises body =
       Future.fork_deps (map snd promises) (fn () =>
-        fulfill_proof thy id (map (apsnd Future.join) promises) body);
+        fulfill_proof thy (map (apsnd Future.join) promises) body);
 
 
 (***** theorems *****)
 
-fun thm_proof thy name hyps prop promises body =
+fun thm_proof thy name hyps concl promises body =
   let
     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
-    val prop = Logic.list_implies (hyps, prop);
+    val prop = Logic.list_implies (hyps, concl);
     val nvs = needed_vars prop;
     val args = map (fn (v as Var (ixn, _)) =>
         if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
@@ -1323,9 +1318,7 @@
       else MinProof;
     val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
 
-    fun new_prf () =
-      let val id = serial ()
-      in (id, name, prop, fulfill_proof_future thy id promises body0) end;
+    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
     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	Thu Oct 01 14:11:28 2009 +0200
+++ b/src/Pure/thm.ML	Thu Oct 01 14:27:50 2009 +0200
@@ -540,7 +540,7 @@
 fun raw_body (Thm (Deriv {body, ...}, _)) = body;
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
-  Pt.fulfill_proof (Theory.deref thy_ref) ~1
+  Pt.fulfill_proof (Theory.deref thy_ref)
     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
 and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));