tuned signature;

--- a/src/Pure/drule.ML	Wed Mar 04 23:14:38 2015 +0100
+++ b/src/Pure/drule.ML	Wed Mar 04 23:21:09 2015 +0100
@@ -773,10 +773,10 @@
 local
   fun add_types (ct, cu) (thy, tye, maxidx) =
     let
-      val {t, T, maxidx = maxt, ...} = Thm.rep_cterm ct;
-      val {t = u, T = U, maxidx = maxu, ...} = Thm.rep_cterm cu;
-      val maxi = Int.max (maxidx, Int.max (maxt, maxu));
-      val thy' = Theory.merge (thy, Theory.merge (Thm.theory_of_cterm ct, Thm.theory_of_cterm cu));
+      val t = Thm.term_of ct and T = Thm.typ_of_cterm ct;
+      val u = Thm.term_of cu and U = Thm.typ_of_cterm cu;
+      val maxi = Int.max (maxidx, Int.max (apply2 Thm.maxidx_of_cterm (ct, cu)));
+      val thy' = Theory.merge (thy, Theory.merge (apply2 Thm.theory_of_cterm (ct, cu)));
       val (tye', maxi') = Sign.typ_unify thy' (T, U) (tye, maxi)
         handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^
           Syntax.string_of_typ_global thy' (Envir.norm_type tye T) ^

--- 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;