--- a/src/Pure/thm.ML Wed Mar 04 23:14:38 2015 +0100
+++ b/src/Pure/thm.ML Wed Mar 04 23:21:09 2015 +0100
@@ -26,7 +26,6 @@
val ctyp_of: theory -> typ -> ctyp
val dest_ctyp: ctyp -> ctyp list
(*certified terms*)
- val rep_cterm: cterm -> {thy: theory, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T}
val theory_of_cterm: cterm -> theory
val term_of: cterm -> term
val typ_of_cterm: cterm -> typ
@@ -174,8 +173,6 @@
exception CTERM of string * cterm list;
-fun rep_cterm (Cterm args) = args;
-
fun theory_of_cterm (Cterm {thy, ...}) = thy;
fun term_of (Cterm {t, ...}) = t;