--- a/src/HOL/Quickcheck.thy Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Quickcheck.thy Fri Aug 27 19:34:23 2010 +0200
@@ -97,7 +97,7 @@
\<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>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"
-instantiation "fun" :: ("{eq, term_of}", random) random
+instantiation "fun" :: ("{equal, term_of}", random) random
begin
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where