src/HOL/Quickcheck.thy
changeset 46664 1f6c140f9c72
parent 46638 fc315796794e
child 46975 c54ca5717f73
--- a/src/HOL/Quickcheck.thy	Fri Feb 24 22:46:16 2012 +0100
+++ b/src/HOL/Quickcheck.thy	Fri Feb 24 22:46:44 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