put_name/thm_proof: promises are filled with fulfilled proofs;
authorwenzelm
Sun Nov 16 22:12:43 2008 +0100 (2008-11-16)
changeset 28816d651b0b15835
parent 28815 80bb72a0f577
child 28817 c8cc94a470d4
put_name/thm_proof: promises are filled with fulfilled proofs;
tuned;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Sun Nov 16 22:12:41 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Sun Nov 16 22:12:43 2008 +0100
     1.3 @@ -1658,12 +1658,10 @@
     1.4  
     1.5  (* fulfilled proof *)
     1.6  
     1.7 -fun deriv_of (Thm (Deriv der, _)) = der;
     1.8 -val raw_proof_of = Proofterm.proof_of o #body o deriv_of;
     1.9 +fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;
    1.10  
    1.11 -fun proof_body_of thm =
    1.12 +fun proof_body_of (Thm (Deriv {all_promises, promises, body}, _)) =
    1.13    let
    1.14 -    val {all_promises, promises, body} = deriv_of thm;
    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    in Pt.fulfill_proof ps body end;
    1.18 @@ -1683,7 +1681,7 @@
    1.19      val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
    1.20  
    1.21      val ps =
    1.22 -      map (apsnd (fn future => Lazy.lazy (fn () => raw_proof_of (Future.join future)))) promises;
    1.23 +      map (apsnd (fn future => Lazy.lazy (fn () => proof_of (Future.join future)))) promises;
    1.24      val thy = Theory.deref thy_ref;
    1.25      val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
    1.26      val der' = make_deriv [] [] [] [pthm] proof;