# HG changeset patch
# User wenzelm
# Date 964954207 -7200
# Node ID 8645b041336610e2025b30a09be97f3d7ccffb6f
# Parent  53d7ad5bec396d07ac76baf3a08ec32bf357c37e
added sign_of_cterm;

diff -r 53d7ad5bec39 -r 8645b0413366 src/Pure/thm.ML
--- 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};