--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 10 14:59:19 2021 +0200
@@ -871,7 +871,7 @@
fun rewrite_pat (ct1, ct2) =
(ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
val t_insts' = map rewrite_pat (Vars.dest t_insts)
- val intro'' = Thm.instantiate (TVars.dest T_insts, t_insts') intro
+ val intro'' = Thm.instantiate (T_insts, Vars.make t_insts') intro
val [intro'''] = Variable.export ctxt3 ctxt [intro'']
val intro'''' =
Simplifier.full_simplify
@@ -941,9 +941,9 @@
val f' = absdummy (U --> T') (Bound 0 $ y)
val th' =
Thm.instantiate
- ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
+ (TVars.make [(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
(dest_TVar uninst_T', Thm.ctyp_of ctxt' T')],
- [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
+ Vars.make [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
in
th'
@@ -1083,13 +1083,16 @@
val instT =
TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T))
(subst_of (pred', pred)) [];
- in Thm.instantiate (instT, []) th end
+ in Thm.instantiate (TVars.make instT, Vars.empty) th end
fun instantiate_ho_args th =
let
val (_, args') =
(strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
val ho_args' = map dest_Var (ho_args_of_typ T args')
- in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end
+ in
+ Thm.instantiate (TVars.empty, Vars.make (ho_args' ~~ map (Thm.cterm_of ctxt') ho_args))
+ th
+ end
val outp_pred =
Term_Subst.instantiate (subst_of (inp_pred, pred), Vars.empty) inp_pred
val ((_, ths'), ctxt1) =