--- 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 =