--- a/src/HOL/Rat.thy Fri Feb 15 08:31:30 2013 +0100
+++ b/src/HOL/Rat.thy Fri Feb 15 08:31:31 2013 +0100
@@ -1031,7 +1031,7 @@
definition
"Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair (
- let j = Code_Numeral.int_of (denom + 1)
+ let j = int_of_integer (integer_of_natural (denom + 1))
in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
instance ..
@@ -1045,7 +1045,8 @@
begin
definition
- "exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive (%l. Quickcheck_Exhaustive.exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
+ "exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive
+ (\<lambda>l. Quickcheck_Exhaustive.exhaustive (\<lambda>k. f (Fract k (int_of_integer (integer_of_natural l) + 1))) d) d"
instance ..
@@ -1056,7 +1057,7 @@
definition
"full_exhaustive_rat f d = Quickcheck_Exhaustive.full_exhaustive (%(l, _). Quickcheck_Exhaustive.full_exhaustive (%k.
- f (let j = Code_Numeral.int_of l + 1
+ f (let j = int_of_integer (integer_of_natural l) + 1
in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d"
instance ..
@@ -1135,3 +1136,4 @@
declare Quotient_rat[quot_del]
end
+