# HG changeset patch
# User bulwahn
# Date 1302180686 -7200
# Node ID 50850486f8dc6535bddbd49e107e3505db636dea
# Parent  3b94cbd903c191b9c0980bc5249813c239f89952
removing instantiation exhaustive for unit in Quickcheck_Exhaustive

diff -r 3b94cbd903c1 -r 50850486f8dc src/HOL/Quickcheck_Exhaustive.thy
--- 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