--- a/src/HOL/Library/DAList.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Library/DAList.thy Thu Nov 12 09:06:44 2020 +0100
@@ -128,9 +128,6 @@
subsection \<open>Quickcheck generators\<close>
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
definition (in term_syntax)
valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where "valterm_empty = Code_Evaluation.valtermify empty"
@@ -142,7 +139,11 @@
('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
-fun (in term_syntax) random_aux_alist
+context
+ includes state_combinator_syntax
+begin
+
+fun random_aux_alist
where
"random_aux_alist i j =
(if i = 0 then Pair valterm_empty
@@ -152,6 +153,8 @@
(\<lambda>v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (\<lambda>a. Pair (valterm_update k v a))))),
(1, Pair valterm_empty)]))"
+end
+
instantiation alist :: (random, random) random
begin
@@ -163,9 +166,6 @@
end
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
instantiation alist :: (exhaustive, exhaustive) exhaustive
begin