src/Pure/thm.ML
changeset 28814 463c9e9111ae
parent 28804 5d3b1df16353
child 28816 d651b0b15835
     1.1 --- a/src/Pure/thm.ML	Sun Nov 16 18:19:27 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Sun Nov 16 20:03:42 2008 +0100
     1.3 @@ -148,7 +148,8 @@
     1.4    val freezeT: thm -> thm
     1.5    val join_futures: theory -> unit
     1.6    val future: (unit -> thm) -> cterm -> thm
     1.7 -  val proof_of: thm -> proof_body
     1.8 +  val proof_body_of: thm -> proof_body
     1.9 +  val proof_of: thm -> proof
    1.10    val extern_oracles: theory -> xstring list
    1.11    val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
    1.12  end;
    1.13 @@ -394,9 +395,6 @@
    1.14  
    1.15  (* basic components *)
    1.16  
    1.17 -fun deriv_of (Thm (Deriv der, _)) = der;
    1.18 -val proof_term_of = Proofterm.proof_of o #body o deriv_of;
    1.19 -
    1.20  val theory_of_thm = Theory.deref o #thy_ref o rep_thm;
    1.21  val maxidx_of = #maxidx o rep_thm;
    1.22  fun maxidx_thm th i = Int.max (maxidx_of th, i);
    1.23 @@ -1660,18 +1658,23 @@
    1.24  
    1.25  (* fulfilled proof *)
    1.26  
    1.27 -fun proof_of thm =
    1.28 +fun deriv_of (Thm (Deriv der, _)) = der;
    1.29 +val raw_proof_of = Proofterm.proof_of o #body o deriv_of;
    1.30 +
    1.31 +fun proof_body_of thm =
    1.32    let
    1.33      val {all_promises, promises, body} = deriv_of thm;
    1.34      val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
    1.35 -    val ps = map (apsnd (Lazy.value o proof_term_of o Future.join)) promises;
    1.36 +    val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises;
    1.37    in Pt.fulfill_proof ps body end;
    1.38  
    1.39 +val proof_of = Proofterm.proof_of o proof_body_of;
    1.40 +
    1.41  
    1.42  (* closed derivations with official name *)
    1.43  
    1.44  fun get_name thm =
    1.45 -  Pt.get_name (hyps_of thm) (prop_of thm) (proof_term_of thm);
    1.46 +  Pt.get_name (hyps_of thm) (prop_of thm) (raw_proof_of thm);
    1.47  
    1.48  fun put_name name (thm as Thm (der, args)) =
    1.49    let
    1.50 @@ -1680,7 +1683,7 @@
    1.51      val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
    1.52  
    1.53      val ps =
    1.54 -      map (apsnd (fn future => Lazy.lazy (fn () => proof_term_of (Future.join future)))) promises;
    1.55 +      map (apsnd (fn future => Lazy.lazy (fn () => raw_proof_of (Future.join future)))) promises;
    1.56      val thy = Theory.deref thy_ref;
    1.57      val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
    1.58      val der' = make_deriv [] [] [] [pthm] proof;