src/Pure/thm.ML

   (*certified terms*)
   type cterm
   exception CTERM of string
   val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
   val crep_cterm        : cterm -> {sign: Sign.sg, t: term, T: ctyp, maxidx: int}
+  val sign_of_cterm	: cterm -> Sign.sg
   val term_of           : cterm -> term
   val cterm_of          : Sign.sg -> term -> cterm
   val ctyp_of_term      : cterm -> ctyp
   val read_cterm        : Sign.sg -> string * typ -> cterm
   val cterm_fun         : (term -> term) -> (cterm -> cterm)

   {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};
 
 fun crep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   {sign = Sign.deref sign_ref, t = t, T = Ctyp {sign_ref = sign_ref, T = T},
     maxidx = maxidx};
+
+fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref;
 
 fun term_of (Cterm {t, ...}) = t;
 
 fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};