diff -r 1491b7209e76 -r 594480d25aaa src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Tue Apr 05 08:53:52 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Apr 05 09:38:23 2011 +0200
@@ -360,18 +360,6 @@
 class bounded_forall =
   fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
 
-
-instantiation nat :: bounded_forall
-begin
-
-fun bounded_forall_nat :: "(nat => bool) => code_numeral => bool"
-where
-  "bounded_forall P d = ((P 0) \<and> (if d > 0 then bounded_forall (%n. P (Suc n)) (d - 1) else True))"
-
-instance ..
-
-end
-
 subsection {* Defining combinators for any first-order data type *}
 
 definition catch_match :: "term list option => term list option => term list option"