src/Pure/thm.ML

                                   prop: term}
   val crep_thm          : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
                                   shyps: sort list, hyps: cterm list, 
                                   prop: cterm}
   val sign_of_thm       : thm -> Sign.sg
-  val stamps_of_thm     : thm -> string ref list
   val transfer		: theory -> thm -> thm
   val tpairs_of         : thm -> (term * term) list
   val prems_of          : thm -> term list
   val nprems_of         : thm -> int
   val concl_of          : thm -> term

 (*errors involving theorems*)
 exception THM of string * int * thm list;
 
 
 fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
-val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm;
 
 (*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]);

 (* Equality *)
 
 (* Definition of the relation =?= *)
 val flexpair_def = fix_shyps [] []
   (Thm{sign_ref= Sign.self_ref Sign.proto_pure, 
-       der = Join(Axiom(pure_thy, "flexpair_def"), []),
+       der = Join(Axiom(Theory.proto_pure, "flexpair_def"), []),
        shyps = [], 
        hyps = [], 
        maxidx = 0,
        prop = term_of (read_cterm Sign.proto_pure
                        ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))});