diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Quickcheck_Random.thy
--- a/src/HOL/Quickcheck_Random.thy	Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Quickcheck_Random.thy	Thu Nov 12 09:06:44 2020 +0100
@@ -8,9 +8,6 @@
 imports Random Code_Evaluation Enum
 begin
 
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
 setup \<open>Code_Target.add_derived_target ("Quickcheck", [(Code_Runtime.target, I)])\<close>
 
 subsection \<open>Catching Match exceptions\<close>
@@ -33,6 +30,10 @@
 instantiation bool :: random
 begin
 
+context
+  includes state_combinator_syntax
+begin
+
 definition
   "random i = Random.range 2 \<circ>\<rightarrow>
     (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
@@ -41,6 +42,8 @@
 
 end
 
+end
+
 instantiation itself :: (typerep) random
 begin
 
@@ -55,6 +58,10 @@
 instantiation char :: random
 begin
 
+context
+  includes state_combinator_syntax
+begin
+
 definition
   "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
 
@@ -62,6 +69,8 @@
 
 end
 
+end
+
 instantiation String.literal :: random
 begin
 
@@ -75,6 +84,10 @@
 instantiation nat :: random
 begin
 
+context
+  includes state_combinator_syntax
+begin
+
 definition random_nat :: "natural \<Rightarrow> Random.seed
   \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
 where
@@ -86,9 +99,15 @@
 
 end
 
+end
+
 instantiation int :: random
 begin
 
+context
+  includes state_combinator_syntax
+begin
+
 definition
   "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
      let j = (if k \<ge> i then int (nat_of_natural (k - i)) else - (int (nat_of_natural (i - k))))
@@ -98,9 +117,15 @@
 
 end
 
+end
+
 instantiation natural :: random
 begin
 
+context
+  includes state_combinator_syntax
+begin
+
 definition random_natural :: "natural \<Rightarrow> Random.seed
   \<Rightarrow> (natural \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
 where
@@ -110,9 +135,15 @@
 
 end
 
+end
+
 instantiation integer :: random
 begin
 
+context
+  includes state_combinator_syntax
+begin
+
 definition random_integer :: "natural \<Rightarrow> Random.seed
   \<Rightarrow> (integer \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
 where
@@ -124,6 +155,8 @@
 
 end
 
+end
+
 
 subsection \<open>Complex generators\<close>
 
@@ -153,9 +186,15 @@
 
 text \<open>Towards type copies and datatypes\<close>
 
+context
+  includes state_combinator_syntax
+begin
+
 definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
   where "collapse f = (f \<circ>\<rightarrow> id)"
 
+end
+
 definition beyond :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   where "beyond k l = (if l > k then l else 0)"
 
@@ -172,6 +211,10 @@
 instantiation set :: (random) random
 begin
 
+context
+  includes state_combinator_syntax
+begin
+
 fun random_aux_set
 where
   "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
@@ -200,6 +243,8 @@
 
 end
 
+end
+
 lemma random_aux_rec:
   fixes random_aux :: "natural \<Rightarrow> 'a"
   assumes "random_aux 0 = rhs 0"
@@ -223,9 +268,6 @@
 
 code_reserved Quickcheck Random_Generators
 
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
 hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
 
 hide_fact (open) collapse_def beyond_def random_fun_lift_def