--- 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])