src/Pure/thm.ML
changeset 28847 648f01ec1794
parent 28842 e44fae2b721d
child 28874 883ec8ee5e6e
equal deleted inserted replaced
28846:9c6025c721d7 28847:648f01ec1794
  1612       CRITICAL (fn () =>
  1612       CRITICAL (fn () =>
  1613         let
  1613         let
  1614           val (finished, unfinished) = List.partition Future.is_finished (! futures);
  1614           val (finished, unfinished) = List.partition Future.is_finished (! futures);
  1615           val _ = futures := unfinished;
  1615           val _ = futures := unfinished;
  1616         in finished end)
  1616         in finished end)
  1617       |> Future.join_results |> null);
  1617       |> Future.join_results |> Exn.release_all |> null);
  1618   in while not (joined ()) do () end;
  1618   in while not (joined ()) do () end;
  1619 
  1619 
  1620 
  1620 
  1621 (* future rule *)
  1621 (* future rule *)
  1622 
  1622 
  1662 fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;
  1662 fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;
  1663 
  1663 
  1664 fun proof_body_of (Thm (Deriv {all_promises, promises, body}, {thy_ref, ...})) =
  1664 fun proof_body_of (Thm (Deriv {all_promises, promises, body}, {thy_ref, ...})) =
  1665   let
  1665   let
  1666     val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
  1666     val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
  1667     val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises;
  1667     val ps = map (apsnd (raw_proof_of o Future.join)) promises;
  1668   in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
  1668   in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
  1669 
  1669 
  1670 val proof_of = Proofterm.proof_of o proof_body_of;
  1670 val proof_of = Proofterm.proof_of o proof_body_of;
  1671 val force_proof = ignore o proof_body_of;
  1671 val force_proof = ignore o proof_body_of;
  1672 
  1672 
  1680   let
  1680   let
  1681     val Deriv {promises, body, ...} = der;
  1681     val Deriv {promises, body, ...} = der;
  1682     val {thy_ref, hyps, prop, tpairs, ...} = args;
  1682     val {thy_ref, hyps, prop, tpairs, ...} = args;
  1683     val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
  1683     val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
  1684 
  1684 
  1685     val ps =
  1685     val ps = Lazy.lazy (fn () => map (apsnd (proof_of o Future.join)) promises);
  1686       map (apsnd (fn future => Lazy.lazy (fn () => proof_of (Future.join future)))) promises;
       
  1687     val thy = Theory.deref thy_ref;
  1686     val thy = Theory.deref thy_ref;
  1688     val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
  1687     val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
  1689     val der' = make_deriv [] [] [] [pthm] proof;
  1688     val der' = make_deriv [] [] [] [pthm] proof;
  1690     val _ = Theory.check_thy thy;
  1689     val _ = Theory.check_thy thy;
  1691   in Thm (der', args) end;
  1690   in Thm (der', args) end;