--- a/src/HOL/Rat.thy Mon Dec 12 12:03:34 2011 +0100
+++ b/src/HOL/Rat.thy Mon Dec 12 13:45:54 2011 +0100
@@ -1158,7 +1158,7 @@
begin
definition
- "exhaustive f d = exhaustive (%l. exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
+ "exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive (%l. Quickcheck_Exhaustive.exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
instance ..
@@ -1168,7 +1168,7 @@
begin
definition
- "full_exhaustive f d = full_exhaustive (%(l, _). full_exhaustive (%k.
+ "full_exhaustive_rat f d = Quickcheck_Exhaustive.full_exhaustive (%(l, _). Quickcheck_Exhaustive.full_exhaustive (%k.
f (let j = Code_Numeral.int_of l + 1
in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d"