src/Pure/thm.ML

   val global_ctyp_of: theory -> typ -> ctyp
   val ctyp_of: Proof.context -> typ -> ctyp
   val dest_ctyp: ctyp -> ctyp list
   val dest_ctypN: int -> ctyp -> ctyp
   val make_ctyp: ctyp -> ctyp list -> ctyp
+  val maxidx_of_ctyp: ctyp -> int
   (*certified terms*)
   val term_of: cterm -> term
   val typ_of_cterm: cterm -> typ
   val ctyp_of_cterm: cterm -> ctyp
   val maxidx_of_cterm: cterm -> int

 
 datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T};
 
 fun typ_of (Ctyp {T, ...}) = T;
 
+fun maxidx_of_ctyp (Ctyp {maxidx, ...}) = maxidx;
+
 fun global_ctyp_of thy raw_T =
   let
     val T = Sign.certify_typ thy raw_T;
     val maxidx = Term.maxidx_of_typ T;
     val sorts = Sorts.insert_typ T [];