--- a/src/HOL/Rat.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Rat.thy Thu Nov 12 09:06:44 2020 +0100
@@ -1004,10 +1004,11 @@
rat \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
+instantiation rat :: random
+begin
-instantiation rat :: random
+context
+ includes state_combinator_syntax
begin
definition
@@ -1020,8 +1021,7 @@
end
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+end
instantiation rat :: exhaustive
begin