src/Pure/thm.ML

                                   prop: cterm}
   exception THM of string * int * thm list
   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
   val prems_of          : thm -> term list
   val nprems_of         : thm -> int

     aconvs (hyps1, hyps2) andalso
     prop1 aconv prop2
   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
     (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) =
   Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);