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