diff -r e7ee815b04bf -r feebdaa346e5 src/HOL/Quickcheck_Random.thy
--- a/src/HOL/Quickcheck_Random.thy	Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Quickcheck_Random.thy	Sun Nov 15 07:17:06 2020 +0000
@@ -201,13 +201,18 @@
 lemma beyond_zero: "beyond k 0 = 0"
   by (simp add: beyond_def)
 
+context
+  includes term_syntax
+begin
 
-definition (in term_syntax) [code_unfold]:
+definition [code_unfold]:
   "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
 
-definition (in term_syntax) [code_unfold]:
+definition [code_unfold]:
   "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
 
+end
+
 instantiation set :: (random) random
 begin