--- a/src/Pure/drule.ML Sat Apr 13 19:58:28 2019 +0200
+++ b/src/Pure/drule.ML Sat Apr 13 21:43:41 2019 +0200
@@ -21,6 +21,7 @@
val implies_intr_list: cterm list -> thm -> thm
val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
thm -> thm
+ val instantiate'_normalize: ctyp option list -> cterm option list -> thm -> thm
val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm
val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
val infer_instantiate': Proof.context -> cterm option list -> thm -> thm
@@ -731,6 +732,9 @@
fun instantiate_normalize instpair th =
Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
+fun instantiate'_normalize Ts ts th =
+ Thm.adjust_maxidx_thm ~1 (Thm.instantiate' Ts ts th COMP_INCR asm_rl);
+
(*instantiation with type-inference for variables*)
fun infer_instantiate_types _ [] th = th
| infer_instantiate_types ctxt args raw_th =