diff -r 8d0294d877bd -r 107941e8fa01 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -96,7 +96,7 @@
     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,
-      subst_v (\<^const>\<open>Code_Numeral.Suc\<close> $ t_k) eq];
+      subst_v \<^Const>\<open>Code_Numeral.Suc for t_k\<close> eq];
     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
     val ((_, (_, eqs2)), lthy') = lthy
       |> BNF_LFP_Compat.primrec_simple