src/Pure/conjunction.ML

 
 
 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;
 
 fun elim th =
   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)
   end;