thm_proof: replaced lazy by composed futures;
authorwenzelm
Tue Jan 27 00:42:12 2009 +0100 (2009-01-27)
changeset 29636d01bada1df33
parent 29635 31d14e9fa0da
child 29637 da018485b89d
child 29638 1f8f3d26a2cf
thm_proof: replaced lazy by composed futures;
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/proofterm.ML	Tue Jan 27 00:29:37 2009 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Tue Jan 27 00:42:12 2009 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4    val promise_proof: theory -> serial -> term -> proof
     1.5    val fulfill_proof: theory -> (serial * proof) list -> proof_body -> proof_body
     1.6    val thm_proof: theory -> string -> term list -> term ->
     1.7 -    (serial * proof) list lazy -> proof_body -> pthm * proof
     1.8 +    (serial * proof future) list -> proof_body -> pthm * proof
     1.9    val get_name: term list -> term -> proof -> string
    1.10  
    1.11    (** rewriting on proof terms **)
    1.12 @@ -1245,8 +1245,9 @@
    1.13        else MinProof;
    1.14  
    1.15      fun new_prf () = (serial (), name, prop,
    1.16 -      Future.fork_pri ~2 (fn () => fulfill_proof thy (Lazy.force promises)
    1.17 -        (PBody {oracles = oracles0, thms = thms0, proof = proof0})));
    1.18 +      Future.fork_deps (map snd promises) (fn () =>
    1.19 +        fulfill_proof thy (map (apsnd Future.join) promises)
    1.20 +          (PBody {oracles = oracles0, thms = thms0, proof = proof0})));
    1.21  
    1.22      val (i, name, prop, body') =
    1.23        (case strip_combt (fst (strip_combP prf)) of
     2.1 --- a/src/Pure/thm.ML	Tue Jan 27 00:29:37 2009 +0100
     2.2 +++ b/src/Pure/thm.ML	Tue Jan 27 00:42:12 2009 +0100
     2.3 @@ -1658,7 +1658,7 @@
     2.4      val {thy_ref, hyps, prop, tpairs, ...} = args;
     2.5      val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
     2.6  
     2.7 -    val ps = Lazy.lazy (fn () => map (apsnd (proof_of o Future.join)) promises);
     2.8 +    val ps = map (apsnd (Future.map proof_of)) promises;
     2.9      val thy = Theory.deref thy_ref;
    2.10      val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
    2.11