# HG changeset patch
# User wenzelm
# Date 1011297856 -3600
# Node ID 37131c76dff6cbc1b732574d7f640dab4bf788f0
# Parent  c69bd9754473b3dac6e26e2e6e2d86152f6e77e6
added prop_of: thm -> term (at last!);

diff -r c69bd9754473 -r 37131c76dff6 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jan 17 21:03:55 2002 +0100
+++ b/src/Pure/thm.ML	Thu Jan 17 21:04:16 2002 +0100
@@ -50,6 +50,7 @@
   type 'a attribute 	(* = 'a * thm -> 'a * thm *)
   val eq_thm		: thm * thm -> bool
   val sign_of_thm       : thm -> Sign.sg
+  val prop_of           : thm -> term
   val transfer_sg	: Sign.sg -> thm -> thm
   val transfer		: theory -> thm -> thm
   val tpairs_of         : thm -> (term * term) list
@@ -324,6 +325,7 @@
   end;
 
 fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
+fun prop_of (Thm {prop, ...}) = prop;
 
 (*merge signatures of two theorems; raise exception if incompatible*)
 fun merge_thm_sgs