# HG changeset patch
# User wenzelm
# Date 1030439131 -7200
# Node ID d14fb18343cbc2e8e7e65aa2b102cfb02c536a27
# Parent  bbd328200a9aefca9d92c138e394f2301d00dd8f
added proof_of;

diff -r bbd328200a9a -r d14fb18343cb src/Pure/thm.ML
--- 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