tuned promise/fullfill;
authorwenzelm
Mon Nov 17 23:17:13 2008 +0100 (2008-11-17)
changeset 28829c67ab5df760b
parent 28828 c25dd83a6f9f
child 28830 261bf00c6ede
tuned promise/fullfill;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Mon Nov 17 23:17:11 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Mon Nov 17 23:17:13 2008 +0100
     1.3 @@ -1643,9 +1643,9 @@
     1.4      val i = serial ();
     1.5      val future = Future.fork_background (future_result i thy sorts prop o make_result);
     1.6      val _ = add_future thy future;
     1.7 -    val promises = [(i, future)];
     1.8 +    val promise = (i, future);
     1.9    in
    1.10 -    Thm (make_deriv promises promises [] [] (Pt.promise_proof i prop),
    1.11 +    Thm (make_deriv [promise] [promise] [] [] (Pt.promise_proof thy i prop),
    1.12       {thy_ref = thy_ref,
    1.13        tags = [],
    1.14        maxidx = maxidx,
    1.15 @@ -1660,11 +1660,11 @@
    1.16  
    1.17  fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;
    1.18  
    1.19 -fun proof_body_of (Thm (Deriv {all_promises, promises, body}, _)) =
    1.20 +fun proof_body_of (Thm (Deriv {all_promises, promises, body}, {thy_ref, ...})) =
    1.21    let
    1.22      val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
    1.23      val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises;
    1.24 -  in Pt.fulfill_proof ps body end;
    1.25 +  in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
    1.26  
    1.27  val proof_of = Proofterm.proof_of o proof_body_of;
    1.28  
    1.29 @@ -1676,7 +1676,7 @@
    1.30  
    1.31  fun put_name name (thm as Thm (der, args)) =
    1.32    let
    1.33 -    val Deriv {all_promises, promises, body} = der;
    1.34 +    val Deriv {promises, body, ...} = der;
    1.35      val {thy_ref, hyps, prop, tpairs, ...} = args;
    1.36      val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
    1.37