| changeset 46635 | cde737f9c911 | 
| parent 46547 | d1dcb91a512e | 
| child 46638 | fc315796794e | 
--- a/src/HOL/Quickcheck.thy Thu Feb 23 21:16:54 2012 +0100 +++ b/src/HOL/Quickcheck.thy Thu Feb 23 21:25:59 2012 +0100 @@ -233,7 +233,7 @@ definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred" where - "iterate_upto f n m = Pair (Code_Numeral.iterate_upto f n m)" + "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)" definition not_randompred :: "unit randompred \<Rightarrow> unit randompred" where