diff -r 3ef6e38c9847 -r 87fc10f5826c src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Oct 28 20:06:29 2021 +0200
@@ -205,16 +205,17 @@
   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 = (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, P), (\<^var>\<open>?Q::bool\<close>, Q)]);
-  in Drule.implies_elim_list (Thm.instantiate inst @{thm conjI}) [thP, thQ] end;
+    val rule = \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q\<close> by (rule conjI)\<close>
+  in Drule.implies_elim_list rule [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 = (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, P), (\<^var>\<open>?Q::bool\<close>, Q)]);
-    val thP = Thm.implies_elim (Thm.instantiate inst @{thm conjunct1}) thPQ;
-    val thQ = Thm.implies_elim (Thm.instantiate inst @{thm conjunct2}) thPQ;
+    val thP =
+      Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> P\<close> by (rule conjunct1)\<close> thPQ;
+    val thQ =
+      Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> Q\<close> by (rule conjunct2)\<close> thPQ;
   in (thP, thQ) end;
 
 fun conj_elims ctxt th =