--- a/src/HOL/Tools/hologic.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/hologic.ML Fri Sep 10 14:59:19 2021 +0200
@@ -205,16 +205,16 @@
let
val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
- val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
- in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
+ val inst = (TVars.empty, Vars.make [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
+ in Drule.implies_elim_list (Thm.instantiate inst @{thm conjI}) [thP, thQ] end;
fun conj_elim ctxt thPQ =
let
val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
- val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
- val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
- val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
+ val inst = (TVars.empty, Vars.make [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
+ val thP = Thm.implies_elim (Thm.instantiate inst @{thm conjunct1}) thPQ;
+ val thQ = Thm.implies_elim (Thm.instantiate inst @{thm conjunct2}) thPQ;
in (thP, thQ) end;
fun conj_elims ctxt th =