diff -r a2106c0d8c45 -r 2b84d34c5d02 src/HOL/ex/Quickcheck.thy
--- a/src/HOL/ex/Quickcheck.thy	Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy	Thu Aug 28 22:09:20 2008 +0200
@@ -250,7 +250,7 @@
 
 fun compile_generator_expr thy prop tys =
   let
-    val f = CodeTarget.eval_term ("Quickcheck.eval_ref", eval_ref) thy
+    val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy
       (mk_generator_expr thy prop tys) [];
   in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;