src/Pure/more_thm.ML

   val aconvc: cterm * cterm -> bool
   val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table
   val add_vars: thm -> cterm Vars.table -> cterm Vars.table
   val dest_funT: ctyp -> ctyp * ctyp
   val strip_type: ctyp -> ctyp list * ctyp
+  val instantiate_ctyp: ctyp TVars.table -> ctyp -> ctyp
   val all_name: Proof.context -> string * cterm -> cterm -> cterm
   val all: Proof.context -> cterm -> cterm -> cterm
   val mk_binop: cterm -> cterm -> cterm -> cterm
   val dest_binop: cterm -> cterm * cterm
   val dest_implies: cterm -> cterm * cterm

         val (cT1, cT2) = dest_funT cT;
         val (cTs, cT') = strip_type cT2
       in (cT1 :: cTs, cT') end
   | _ => ([], cT));
 
+fun instantiate_ctyp instT cT =
+  Thm.instantiate_cterm (instT, Vars.empty) (Thm.var (("x", 0), cT))
+  |> Thm.ctyp_of_cterm;
+
 
 (* cterm operations *)
 
 fun all_name ctxt (x, t) A =
   let