--- a/src/Pure/more_thm.ML Thu Oct 21 18:20:08 2021 +0200
+++ b/src/Pure/more_thm.ML Sun Oct 24 16:38:13 2021 +0200
@@ -25,6 +25,7 @@
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
@@ -156,6 +157,10 @@
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 *)