--- a/src/Pure/thm.ML Tue Aug 27 11:05:13 2002 +0200
+++ b/src/Pure/thm.ML Tue Aug 27 11:05:31 2002 +0200
@@ -51,6 +51,7 @@
val eq_thm : thm * thm -> bool
val sign_of_thm : thm -> Sign.sg
val prop_of : thm -> term
+ val proof_of : thm -> Proofterm.proof
val transfer_sg : Sign.sg -> thm -> thm
val transfer : theory -> thm -> thm
val tpairs_of : thm -> (term * term) list
@@ -326,6 +327,7 @@
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
fun prop_of (Thm {prop, ...}) = prop;
+fun proof_of (Thm {der = (_, proof), ...}) = proof;
(*merge signatures of two theorems; raise exception if incompatible*)
fun merge_thm_sgs