added sign_of_cterm;

--- a/src/Pure/thm.ML	Sun Jul 30 12:48:55 2000 +0200
+++ b/src/Pure/thm.ML	Sun Jul 30 12:50:07 2000 +0200
@@ -21,6 +21,7 @@
   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
@@ -227,6 +228,8 @@
   {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};