--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Oct 21 09:51:45 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Oct 21 10:32:42 2011 +0200
@@ -1045,9 +1045,9 @@
fun test_goals ctxt (limit_time, is_interactive) insts goals =
let
- val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals
+ val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
in
- Quickcheck.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
+ Quickcheck_Common.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
end