--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Thu Feb 23 21:16:54 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Thu Feb 23 21:25:59 2012 +0100
@@ -30,7 +30,7 @@
HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
fun mk_iterate_upto T (f, from, to) =
- list_comb (Const (@{const_name Code_Numeral.iterate_upto},
+ list_comb (Const (@{const_name Predicate.iterate_upto},
[@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_monadT T),
[f, from, to])