--- a/src/HOL/Quickcheck_Random.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Quickcheck_Random.thy Wed Jan 10 15:25:09 2018 +0100
@@ -136,7 +136,7 @@
\<Rightarrow> Random.seed \<Rightarrow> (('a::term_of \<Rightarrow> 'b::typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
where
"random_fun_lift f =
- random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
+ random_fun_aux TYPEREP('a) TYPEREP('b) (=) Code_Evaluation.term_of f Random.split_seed"
instantiation "fun" :: ("{equal, term_of}", random) random
begin