diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -82,7 +82,7 @@
 val rew_thms = map mk_meta_eq [@{thm natural_zero_minus_one},
   @{thm Suc_natural_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}];
 val rew_ts = map (Logic.dest_equals o Thm.prop_of) rew_thms;
-val rew_ss = simpset_of (put_simpset HOL_ss @{context} addsimps rew_thms);
+val rew_ss = simpset_of (put_simpset HOL_ss \<^context> addsimps rew_thms);
 
 in