diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -92,7 +92,7 @@
       (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
     val Type (_, [_, iT]) = T;
     val icT = Thm.ctyp_of lthy iT;
-    val inst = Thm.instantiate_cterm ([(a_v, icT)], []);
+    val inst = Thm.instantiate_cterm (TVars.make [(a_v, icT)], Vars.empty);
     fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
     val t_rhs = lambda t_k proto_t_rhs;
     val eqs0 = [subst_v \<^term>\<open>0::natural\<close> eq,
@@ -105,8 +105,8 @@
     val cT_rhs = inst pt_rhs |> Thm.term_of |> dest_Var;
     val rule = @{thm random_aux_rec}
       |> Drule.instantiate_normalize
-        ([(a_v, icT)],
-          [(cT_random_aux, Thm.cterm_of lthy' t_random_aux),
+        (TVars.make [(a_v, icT)],
+          Vars.make [(cT_random_aux, Thm.cterm_of lthy' t_random_aux),
            (cT_rhs, Thm.cterm_of lthy' t_rhs)]);
     fun tac ctxt =
       ALLGOALS (resolve_tac ctxt [rule])