fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
authorwenzelm
Wed Mar 25 16:54:17 2009 +0100 (2009-03-25)
changeset 30717465093aa5844
parent 30716 2ee706293eb5
child 30718 15041c7e51e4
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
more explicit oracle_proof;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Wed Mar 25 16:52:50 2009 +0100
     1.2 +++ b/src/Pure/thm.ML	Wed Mar 25 16:54:17 2009 +0100
     1.3 @@ -1662,7 +1662,7 @@
     1.4  fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
     1.5    let
     1.6      val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
     1.7 -    val ps = map (apsnd (raw_proof_of o Future.join)) promises;
     1.8 +    val ps = map (apsnd (raw_proof_body_of o Future.join)) promises;
     1.9    in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
    1.10  
    1.11  val proof_of = Proofterm.proof_of o proof_body_of;
    1.12 @@ -1680,7 +1680,7 @@
    1.13      val {thy_ref, hyps, prop, tpairs, ...} = args;
    1.14      val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
    1.15  
    1.16 -    val ps = map (apsnd (Future.map proof_of)) promises;
    1.17 +    val ps = map (apsnd (Future.map proof_body_of)) promises;
    1.18      val thy = Theory.deref thy_ref;
    1.19      val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
    1.20  
    1.21 @@ -1701,8 +1701,8 @@
    1.22      if T <> propT then
    1.23        raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
    1.24      else
    1.25 -      let val prf = Pt.oracle_proof name prop in
    1.26 -        Thm (make_deriv ~1 [] [] (Pt.make_oracles prf) [] prf,
    1.27 +      let val (ora, prf) = Pt.oracle_proof name prop in
    1.28 +        Thm (make_deriv ~1 [] [] [ora] [] prf,
    1.29           {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
    1.30            tags = [],
    1.31            maxidx = maxidx,