diff -r bb39fba83e9b -r 53a697f5454a src/HOL/Rat.thy
--- 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"