fulfill_proof/thm_proof: commuted lazyness;
authorwenzelm
Tue Nov 18 22:25:36 2008 +0100 (2008-11-18)
changeset 28847648f01ec1794
parent 28846 9c6025c721d7
child 28848 9a02932efb91
fulfill_proof/thm_proof: commuted lazyness;
join_futures: Exn.release_all is back again (still required for implicit join of Toplevel.excursion);
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Tue Nov 18 22:25:30 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Tue Nov 18 22:25:36 2008 +0100
     1.3 @@ -1614,7 +1614,7 @@
     1.4            val (finished, unfinished) = List.partition Future.is_finished (! futures);
     1.5            val _ = futures := unfinished;
     1.6          in finished end)
     1.7 -      |> Future.join_results |> null);
     1.8 +      |> Future.join_results |> Exn.release_all |> null);
     1.9    in while not (joined ()) do () end;
    1.10  
    1.11  
    1.12 @@ -1664,7 +1664,7 @@
    1.13  fun proof_body_of (Thm (Deriv {all_promises, promises, body}, {thy_ref, ...})) =
    1.14    let
    1.15      val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
    1.16 -    val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises;
    1.17 +    val ps = map (apsnd (raw_proof_of o Future.join)) promises;
    1.18    in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
    1.19  
    1.20  val proof_of = Proofterm.proof_of o proof_body_of;
    1.21 @@ -1682,8 +1682,7 @@
    1.22      val {thy_ref, hyps, prop, tpairs, ...} = args;
    1.23      val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
    1.24  
    1.25 -    val ps =
    1.26 -      map (apsnd (fn future => Lazy.lazy (fn () => proof_of (Future.join future)))) promises;
    1.27 +    val ps = Lazy.lazy (fn () => map (apsnd (proof_of o Future.join)) promises);
    1.28      val thy = Theory.deref thy_ref;
    1.29      val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
    1.30      val der' = make_deriv [] [] [] [pthm] proof;