--- a/src/Pure/conjunction.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/conjunction.ML Fri Sep 10 14:59:19 2021 +0200
@@ -102,7 +102,8 @@
fun intr tha thb =
Thm.implies_elim
(Thm.implies_elim
- (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
+ (Thm.instantiate (TVars.empty, Vars.make [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)])
+ conjunctionI)
tha)
thb;
@@ -110,7 +111,7 @@
let
val (A, B) = dest_conjunction (Thm.cprop_of th)
handle TERM (msg, _) => raise THM (msg, 0, [th]);
- val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
+ val inst = Thm.instantiate (TVars.empty, Vars.make [(vA, A), (vB, B)]);
in
(Thm.implies_elim (inst conjunctionD1) th,
Thm.implies_elim (inst conjunctionD2) th)