--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Oct 16 21:49:47 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Oct 17 10:19:01 2011 +0200
@@ -462,9 +462,9 @@
fun test_goals ctxt (limit_time, is_interactive) insts goals =
if (not (getenv "ISABELLE_GHC" = "")) then
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
else
(if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message