--- a/src/Pure/variable.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/variable.ML Fri Sep 10 14:59:19 2021 +0200
@@ -618,7 +618,7 @@
let
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT;
- val ths' = map (Thm.instantiate (TVars.dest instT', [])) ths;
+ val ths' = map (Thm.instantiate (instT', Vars.empty)) ths;
in ((instT', ths'), ctxt') end;
fun import_prf is_open prf ctxt =
@@ -632,7 +632,7 @@
val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT;
val inst' = Vars.map (K (Thm.cterm_of ctxt')) inst;
- val ths' = map (Thm.instantiate (TVars.dest instT', Vars.dest inst')) ths;
+ val ths' = map (Thm.instantiate (instT', inst')) ths;
in (((instT', inst'), ths'), ctxt') end;
fun import_vars ctxt th =