--- a/src/HOL/Library/FSet.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Library/FSet.thy Thu Nov 12 09:06:44 2020 +0100
@@ -1342,9 +1342,11 @@
no_notation Quickcheck_Exhaustive.orelse (infixr "orelse" 55)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
+instantiation fset :: (random) random
+begin
-instantiation fset :: (random) random
+context
+ includes state_combinator_syntax
begin
fun random_aux_fset :: "natural \<Rightarrow> natural \<Rightarrow> natural \<times> natural \<Rightarrow> ('a fset \<times> (unit \<Rightarrow> term)) \<times> natural \<times> natural" where
@@ -1373,6 +1375,6 @@
end
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+end
end