--- a/src/HOL/Quickcheck_Exhaustive.thy Thu Apr 07 14:51:25 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Thu Apr 07 14:51:26 2011 +0200
@@ -18,15 +18,6 @@
class exhaustive = term_of +
fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
-instantiation unit :: exhaustive
-begin
-
-definition "exhaustive f d = f (Code_Evaluation.valtermify ())"
-
-instance ..
-
-end
-
instantiation code_numeral :: exhaustive
begin