# HG changeset patch
# User bulwahn
# Date 1319185962 -7200
# Node ID 026a7619936fdcbf3aac73b2d567dddcc8def080
# Parent  7da4e22714fba597e7ef158d3878d931bdf66d89
correcting code_prolog

diff -r 7da4e22714fb -r 026a7619936f src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- 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