diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/Quickcheck_Random.thy
--- 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