# HG changeset patch
# User wenzelm
# Date 880558684 -3600
# Node ID 3f5e8c4aa84d20f0284df8e8b88f820052bf317f
# Parent  227a9e786c35721408a9d48a8a422b81644cec20
added crep_cterm;

diff -r 227a9e786c35 -r 3f5e8c4aa84d src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Nov 26 16:37:43 1997 +0100
+++ b/src/Pure/thm.ML	Wed Nov 26 16:38:04 1997 +0100
@@ -20,6 +20,7 @@
   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 term_of           : cterm -> term
   val cterm_of          : Sign.sg -> term -> cterm
   val ctyp_of_term      : cterm -> ctyp
@@ -203,6 +204,10 @@
 fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   {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 term_of (Cterm {t, ...}) = t;
 
 fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};