src/HOL/Quickcheck_Exhaustive.thy

--- a/src/HOL/Quickcheck_Exhaustive.thy	Tue Dec 20 17:22:31 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Dec 20 17:39:56 2011 +0100
@@ -4,7 +4,9 @@
 
 theory Quickcheck_Exhaustive
 imports Quickcheck
-uses ("Tools/Quickcheck/exhaustive_generators.ML")
+uses
+  ("Tools/Quickcheck/exhaustive_generators.ML")
+  ("Tools/Quickcheck/abstract_generators.ML")
 begin
 
 subsection {* basic operations for exhaustive generators *}
@@ -521,7 +523,7 @@
 where
   "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
 
-subsection {* Defining combinators for any first-order data type *}
+subsection {* Defining generators for any first-order data type *}
 
 axiomatization unknown :: 'a
 
@@ -533,6 +535,10 @@
 
 declare [[quickcheck_batch_tester = exhaustive]]
 
+subsection {* Defining generators for abstract types *}
+
+use "Tools/Quickcheck/abstract_generators.ML"
+
 hide_fact orelse_def
 no_notation orelse (infixr "orelse" 55)