diff -r 531a0c44ea3f -r de581f98a3a1 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Real.thy	Thu Nov 12 09:06:44 2020 +0100
@@ -1638,10 +1638,11 @@
   valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)"
   where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
 
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
+instantiation real :: random
+begin
 
-instantiation real :: random
+context
+  includes state_combinator_syntax
 begin
 
 definition
@@ -1651,8 +1652,7 @@
 
 end
 
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+end
 
 instantiation real :: exhaustive
 begin